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

Theorem lclkrlem2b 34541
 Description: Lemma for lclkr 34566. (Contributed by NM, 17-Jan-2015.)
Hypotheses
Ref Expression
lclkrlem2a.h
lclkrlem2a.o
lclkrlem2a.u
lclkrlem2a.v
lclkrlem2a.z
lclkrlem2a.p
lclkrlem2a.n
lclkrlem2a.a LSAtoms
lclkrlem2a.k
lclkrlem2a.b
lclkrlem2a.x
lclkrlem2a.y
lclkrlem2a.e
lclkrlem2b.da
Assertion
Ref Expression
lclkrlem2b

Proof of Theorem lclkrlem2b
StepHypRef Expression
1 lclkrlem2a.h . . 3
2 lclkrlem2a.o . . 3
3 lclkrlem2a.u . . 3
4 lclkrlem2a.v . . 3
5 lclkrlem2a.z . . 3
6 lclkrlem2a.p . . 3
7 lclkrlem2a.n . . 3
8 lclkrlem2a.a . . 3 LSAtoms
9 lclkrlem2a.k . . . 4
11 lclkrlem2a.b . . . 4
13 lclkrlem2a.x . . . 4
15 lclkrlem2a.y . . . 4
17 lclkrlem2a.e . . . 4
19 simpr 461 . . 3
201, 2, 3, 4, 5, 6, 7, 8, 10, 12, 14, 16, 18, 19lclkrlem2a 34540 . 2
211, 3, 9dvhlmod 34143 . . . . . . 7
22 lmodabl 17879 . . . . . . 7
2321, 22syl 17 . . . . . 6
24 eqid 2404 . . . . . . . . 9
2524lsssssubg 17926 . . . . . . . 8 SubGrp
2621, 25syl 17 . . . . . . 7 SubGrp
2713eldifad 3428 . . . . . . . 8
284, 24, 7lspsncl 17945 . . . . . . . 8
2921, 27, 28syl2anc 661 . . . . . . 7
3026, 29sseldd 3445 . . . . . 6 SubGrp
3115eldifad 3428 . . . . . . . 8
324, 24, 7lspsncl 17945 . . . . . . . 8
3321, 31, 32syl2anc 661 . . . . . . 7
3426, 33sseldd 3445 . . . . . 6 SubGrp
356lsmcom 17190 . . . . . 6 SubGrp SubGrp
3623, 30, 34, 35syl3anc 1232 . . . . 5
3736ineq1d 3642 . . . 4