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

Theorem erngdvlem3-rN 34565
 Description: Lemma for eringring 34559. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
ernggrp.h-r
ernggrp.d-r
ernggrplem.b-r
ernggrplem.t-r
ernggrplem.e-r
ernggrplem.p-r
ernggrplem.o-r
ernggrplem.i-r
erngrnglem.m-r
Assertion
Ref Expression
erngdvlem3-rN
Distinct variable groups:   ,   ,,   ,,,   ,   ,,,   ,,,
Allowed substitution hints:   (,)   (,,)   (,,)   ()   (,)   (,,)   (,,)   (,,)

Proof of Theorem erngdvlem3-rN
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ernggrp.h-r . . . 4
2 ernggrplem.t-r . . . 4
3 ernggrplem.e-r . . . 4
4 ernggrp.d-r . . . 4
5 eqid 2451 . . . 4
61, 2, 3, 4, 5erngbase-rN 34376 . . 3
76eqcomd 2457 . 2
8 eqid 2451 . . . 4
91, 2, 3, 4, 8erngfplus-rN 34377 . . 3
10 ernggrplem.p-r . . 3
119, 10syl6reqr 2504 . 2
12 eqid 2451 . . . 4
131, 2, 3, 4, 12erngfmul-rN 34380 . . 3
14 erngrnglem.m-r . . 3
1513, 14syl6reqr 2504 . 2
16 ernggrplem.b-r . . 3
17 ernggrplem.o-r . . 3
18 ernggrplem.i-r . . 3
191, 4, 16, 2, 3, 10, 17, 18erngdvlem1-rN 34563 . 2
2015oveqd 6307 . . . . 5
21203ad2ant1 1029 . . . 4
221, 2, 3, 4, 12erngmul-rN 34381 . . . . 5
23223impb 1204 . . . 4
2421, 23eqtrd 2485 . . 3
251, 3tendococl 34339 . . . 4
26253com23 1214 . . 3
2724, 26eqeltrd 2529 . 2
2815oveqdr 6314 . . . . 5
291, 2, 3, 4, 12erngmul-rN 34381 . . . . . 6
30293adantr1 1167 . . . . 5
3128, 30eqtrd 2485 . . . 4
3231coeq1d 4996 . . 3
3315oveqd 6307 . . . . 5
3433adantr 467 . . . 4
35 simpl 459 . . . . 5
36 simpr1 1014 . . . . 5
37 simpr3 1016 . . . . . . 7
38 simpr2 1015 . . . . . . 7
391, 3tendococl 34339 . . . . . . 7
4035, 37, 38, 39syl3anc 1268 . . . . . 6
4131, 40eqeltrd 2529 . . . . 5
421, 2, 3, 4, 12erngmul-rN 34381 . . . . 5
4335, 36, 41, 42syl12anc 1266 . . . 4
4434, 43eqtrd 2485 . . 3
4515oveqd 6307 . . . . . 6
4645adantr 467 . . . . 5
47273adant3r3 1219 . . . . . 6
481, 2, 3, 4, 12erngmul-rN 34381 . . . . . 6
4935, 47, 37, 48syl12anc 1266 . . . . 5
5015oveqdr 6314 . . . . . . 7
51223adantr3 1169 . . . . . . 7
5250, 51eqtrd 2485 . . . . . 6
5352coeq2d 4997 . . . . 5
5446, 49, 533eqtrd 2489 . . . 4
55 coass 5354 . . . 4
5654, 55syl6eqr 2503 . . 3
5732, 44, 563eqtr4rd 2496 . 2
581, 2, 3, 10tendodi2 34352 . . . 4
5935, 38, 37, 36, 58syl13anc 1270 . . 3
6015oveqd 6307 . . . . 5
6160adantr 467 . . . 4
621, 2, 3, 10tendoplcl 34348 . . . . . 6
6335, 38, 37, 62syl3anc 1268 . . . . 5
641, 2, 3, 4, 12erngmul-rN 34381 . . . . 5
6535, 36, 63, 64syl12anc 1266 . . . 4
6661, 65eqtrd 2485 . . 3
6715oveqdr 6314 . . . . 5
681, 2, 3, 4, 12erngmul-rN 34381 . . . . . 6
69683adantr2 1168 . . . . 5
7067, 69eqtrd 2485 . . . 4
7152, 70oveq12d 6308 . . 3
7259, 66, 713eqtr4d 2495 . 2
731, 2, 3, 10tendodi1 34351 . . . 4
7435, 37, 36, 38, 73syl13anc 1270 . . 3
7515adantr 467 . . . . 5
7675oveqd 6307 . . . 4
771, 2, 3, 10tendoplcl 34348 . . . . . 6
78773adant3r3 1219 . . . . 5
791, 2, 3, 4, 12erngmul-rN 34381 . . . . 5
8035, 78, 37, 79syl12anc 1266 . . . 4
8176, 80eqtrd 2485 . . 3
8270, 31oveq12d 6308 . . 3
8374, 81, 823eqtr4d 2495 . 2
841, 2, 3tendoidcl 34336 . 2
8515oveqd 6307 . . . 4
87 simpl 459 . . . 4
8884adantr 467 . . . 4
89 simpr 463 . . . 4
901, 2, 3, 4, 12erngmul-rN 34381 . . . 4
9187, 88, 89, 90syl12anc 1266 . . 3
921, 2, 3tendo1mulr 34338 . . 3
9386, 91, 923eqtrd 2489 . 2
9415oveqd 6307 . . . 4