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

Theorem erngdvlem3-rN 31732
 Description: Lemma for erngrng 31726. (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 2435 . . . 4
61, 2, 3, 4, 5erngbase-rN 31543 . . 3
76eqcomd 2440 . 2
8 eqid 2435 . . . 4
91, 2, 3, 4, 8erngfplus-rN 31544 . . 3
10 ernggrplem.p-r . . 3
119, 10syl6reqr 2486 . 2
12 eqid 2435 . . . 4
131, 2, 3, 4, 12erngfmul-rN 31547 . . 3
14 erngrnglem.m-r . . 3
1513, 14syl6reqr 2486 . 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 31730 . 2
2015oveqd 6090 . . . . 5
21203ad2ant1 978 . . . 4
221, 2, 3, 4, 12erngmul-rN 31548 . . . . 5
23223impb 1149 . . . 4
2421, 23eqtrd 2467 . . 3
251, 3tendococl 31506 . . . 4
26253com23 1159 . . 3
2724, 26eqeltrd 2509 . 2
2815proplem3 13908 . . . . 5
291, 2, 3, 4, 12erngmul-rN 31548 . . . . . 6
30293adantr1 1116 . . . . 5
3128, 30eqtrd 2467 . . . 4
3231coeq1d 5026 . . 3
3315oveqd 6090 . . . . 5
3433adantr 452 . . . 4
35 simpl 444 . . . . 5
36 simpr1 963 . . . . 5
37 simpr3 965 . . . . . . 7
38 simpr2 964 . . . . . . 7
391, 3tendococl 31506 . . . . . . 7
4035, 37, 38, 39syl3anc 1184 . . . . . 6
4131, 40eqeltrd 2509 . . . . 5
421, 2, 3, 4, 12erngmul-rN 31548 . . . . 5
4335, 36, 41, 42syl12anc 1182 . . . 4
4434, 43eqtrd 2467 . . 3
4515oveqd 6090 . . . . . 6
4645adantr 452 . . . . 5
47273adant3r3 1164 . . . . . 6
481, 2, 3, 4, 12erngmul-rN 31548 . . . . . 6
4935, 47, 37, 48syl12anc 1182 . . . . 5
5015proplem3 13908 . . . . . . 7
51223adantr3 1118 . . . . . . 7
5250, 51eqtrd 2467 . . . . . 6
5352coeq2d 5027 . . . . 5
5446, 49, 533eqtrd 2471 . . . 4
55 coass 5380 . . . 4
5654, 55syl6eqr 2485 . . 3
5732, 44, 563eqtr4rd 2478 . 2
581, 2, 3, 10tendodi2 31519 . . . 4
5935, 38, 37, 36, 58syl13anc 1186 . . 3
6015oveqd 6090 . . . . 5
6160adantr 452 . . . 4
621, 2, 3, 10tendoplcl 31515 . . . . . 6
6335, 38, 37, 62syl3anc 1184 . . . . 5
641, 2, 3, 4, 12erngmul-rN 31548 . . . . 5
6535, 36, 63, 64syl12anc 1182 . . . 4
6661, 65eqtrd 2467 . . 3
6715proplem3 13908 . . . . 5
681, 2, 3, 4, 12erngmul-rN 31548 . . . . . 6
69683adantr2 1117 . . . . 5
7067, 69eqtrd 2467 . . . 4
7152, 70oveq12d 6091 . . 3
7259, 66, 713eqtr4d 2477 . 2
731, 2, 3, 10tendodi1 31518 . . . 4
7435, 37, 36, 38, 73syl13anc 1186 . . 3
7515adantr 452 . . . . 5
7675oveqd 6090 . . . 4
771, 2, 3, 10tendoplcl 31515 . . . . . 6
78773adant3r3 1164 . . . . 5
791, 2, 3, 4, 12erngmul-rN 31548 . . . . 5
8035, 78, 37, 79syl12anc 1182 . . . 4
8176, 80eqtrd 2467 . . 3
8270, 31oveq12d 6091 . . 3
8374, 81, 823eqtr4d 2477 . 2
841, 2, 3tendoidcl 31503 . 2
8515oveqd 6090 . . . 4
87 simpl 444 . . . 4
8884adantr 452 . . . 4
89 simpr 448 . . . 4
901, 2, 3, 4, 12erngmul-rN 31548 . . . 4
9187, 88, 89, 90syl12anc 1182 . . 3
921, 2, 3tendo1mulr 31505 . . 3
9386, 91, 923eqtrd 2471 . 2
9415oveqd 6090 . . . 4