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

Theorem cdleme20y 30491
 Description: Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.)
Hypotheses
Ref Expression
cdleme20z.l
cdleme20z.j
cdleme20z.m
cdleme20z.a
Assertion
Ref Expression
cdleme20y

Proof of Theorem cdleme20y
StepHypRef Expression
1 simp3r 984 . . . . . 6
2 simp1 955 . . . . . . . 8
3 simp22 989 . . . . . . . 8
4 simp23 990 . . . . . . . 8
5 cdleme20z.j . . . . . . . . 9
6 cdleme20z.a . . . . . . . . 9
75, 6hlatjcom 29557 . . . . . . . 8
82, 3, 4, 7syl3anc 1182 . . . . . . 7
98breq2d 4035 . . . . . 6
101, 9mtbid 291 . . . . 5
11 hlcvl 29549 . . . . . . 7
12113ad2ant1 976 . . . . . 6
13 simp21 988 . . . . . 6
14 simp3l 983 . . . . . 6
15 cdleme20z.l . . . . . . 7
1615, 5, 6cvlatexch1 29526 . . . . . 6
1712, 3, 13, 4, 14, 16syl131anc 1195 . . . . 5
1810, 17mtod 168 . . . 4
19 hlatl 29550 . . . . . 6
20193ad2ant1 976 . . . . 5
21 eqid 2283 . . . . . . 7
2221, 5, 6hlatjcl 29556 . . . . . 6
232, 4, 13, 22syl3anc 1182 . . . . 5
24 cdleme20z.m . . . . . 6
25 eqid 2283 . . . . . 6
2621, 15, 24, 25, 6atnle 29507 . . . . 5
2720, 3, 23, 26syl3anc 1182 . . . 4
2818, 27mpbid 201 . . 3
2928oveq1d 5873 . 2
3021, 6atbase 29479 . . . 4
3113, 30syl 15 . . 3
3215, 5, 6hlatlej2 29565 . . . 4
332, 4, 13, 32syl3anc 1182 . . 3
3421, 15, 5, 24, 6atmod4i2 30056 . . 3
352, 3, 31, 23, 33, 34syl131anc 1195 . 2
36 hlol 29551 . . . 4