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

Theorem lclkrlem2b 31071
 Description: Lemma for lclkr 31096. (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 447 . . 3
201, 2, 3, 4, 5, 6, 7, 8, 10, 12, 14, 16, 18, 19lclkrlem2a 31070 . 2
211, 3, 9dvhlmod 30673 . . . . . . 7
22 lmodabl 15672 . . . . . . 7
2321, 22syl 15 . . . . . 6
24 eqid 2283 . . . . . . . . 9
2524lsssssubg 15715 . . . . . . . 8 SubGrp
2621, 25syl 15 . . . . . . 7 SubGrp
27 eldifi 3298 . . . . . . . . 9
2813, 27syl 15 . . . . . . . 8
294, 24, 7lspsncl 15734 . . . . . . . 8
3021, 28, 29syl2anc 642 . . . . . . 7
3126, 30sseldd 3181 . . . . . 6 SubGrp
32 eldifi 3298 . . . . . . . . 9
3315, 32syl 15 . . . . . . . 8
344, 24, 7lspsncl 15734 . . . . . . . 8
3521, 33, 34syl2anc 642 . . . . . . 7
3626, 35sseldd 3181 . . . . . 6 SubGrp
376lsmcom 15150 . . . . . 6 SubGrp SubGrp
3823, 31, 36, 37syl3anc 1182 . . . . 5
3938ineq1d 3369 . . . 4