Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme50ltrn Unicode version

Theorem cdleme50ltrn 29435
 Description: Part of proof of Lemma E in [Crawley] p. 113. is a lattice translation. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
Hypotheses
Ref Expression
cdlemef50.b
cdlemef50.l
cdlemef50.j
cdlemef50.m
cdlemef50.a
cdlemef50.h
cdlemef50.u
cdlemef50.d
cdlemefs50.e
cdlemef50.f
cdleme50ltrn.t
Assertion
Ref Expression
cdleme50ltrn
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,   ,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   (,,,,)   (,)   (,,,,)

Proof of Theorem cdleme50ltrn
StepHypRef Expression
1 cdlemef50.b . . 3
2 cdlemef50.l . . 3
3 cdlemef50.j . . 3
4 cdlemef50.m . . 3
5 cdlemef50.a . . 3
6 cdlemef50.h . . 3
7 cdlemef50.u . . 3
8 cdlemef50.d . . 3
9 cdlemefs50.e . . 3
10 cdlemef50.f . . 3
11 eqid 2253 . . 3
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11cdleme50ldil 29426 . 2
13 simp1 960 . . . . . 6
14 simp2l 986 . . . . . 6
15 simp3l 988 . . . . . 6
161, 2, 3, 4, 5, 6, 7, 8, 9, 10cdleme50trn123 29432 . . . . . 6
1713, 14, 15, 16syl12anc 1185 . . . . 5
18 simp2r 987 . . . . . 6
19 simp3r 989 . . . . . 6
201, 2, 3, 4, 5, 6, 7, 8, 9, 10cdleme50trn123 29432 . . . . . 6
2113, 18, 19, 20syl12anc 1185 . . . . 5
2217, 21eqtr4d 2288 . . . 4
23223exp 1155 . . 3
2423ralrimivv 2596 . 2
25 cdleme50ltrn.t . . . 4
262, 3, 4, 5, 6, 11, 25isltrn 28997 . . 3