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

Theorem cdleme50ltrn 31039
 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
Dummy variables are mutually distinct and distinct from all other variables.
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 2404 . . 3
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11cdleme50ldil 31030 . 2
13 simp1 957 . . . . . 6
14 simp2l 983 . . . . . 6
15 simp3l 985 . . . . . 6
161, 2, 3, 4, 5, 6, 7, 8, 9, 10cdleme50trn123 31036 . . . . . 6
1713, 14, 15, 16syl12anc 1182 . . . . 5
18 simp2r 984 . . . . . 6
19 simp3r 986 . . . . . 6
201, 2, 3, 4, 5, 6, 7, 8, 9, 10cdleme50trn123 31036 . . . . . 6
2113, 18, 19, 20syl12anc 1182 . . . . 5
2217, 21eqtr4d 2439 . . . 4
23223exp 1152 . . 3
2423ralrimivv 2757 . 2
25 cdleme50ltrn.t . . . 4
262, 3, 4, 5, 6, 11, 25isltrn 30601 . . 3