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

Theorem erngdvlem3 31688
 Description: Lemma for erngrng 31690. (Contributed by NM, 6-Aug-2013.)
Hypotheses
Ref Expression
ernggrp.h
ernggrp.d
erngdv.b
erngdv.t
erngdv.e
erngdv.p
erngdv.o
erngdv.i
erngrnglem.m
Assertion
Ref Expression
erngdvlem3
Distinct variable groups:   ,   ,,   ,,,   ,   ,,,   ,,,
Allowed substitution hints:   (,)   (,,)   (,,)   (,,)   ()   (,)   (,,)   (,,)

Proof of Theorem erngdvlem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ernggrp.h . . . 4
2 erngdv.t . . . 4
3 erngdv.e . . . 4
4 ernggrp.d . . . 4
5 eqid 2435 . . . 4
61, 2, 3, 4, 5erngbase 31499 . . 3
76eqcomd 2440 . 2
8 eqid 2435 . . . 4
91, 2, 3, 4, 8erngfplus 31500 . . 3
10 erngdv.p . . 3
119, 10syl6reqr 2486 . 2
12 eqid 2435 . . . 4
131, 2, 3, 4, 12erngfmul 31503 . . 3
14 erngrnglem.m . . 3
1513, 14syl6reqr 2486 . 2
16 erngdv.b . . 3
17 erngdv.o . . 3
18 erngdv.i . . 3
191, 4, 16, 2, 3, 10, 17, 18erngdvlem1 31686 . 2
2015oveqd 6090 . . . . 5
21203ad2ant1 978 . . . 4
221, 2, 3, 4, 12erngmul 31504 . . . . 5
23223impb 1149 . . . 4
2421, 23eqtrd 2467 . . 3
251, 3tendococl 31470 . . 3
2624, 25eqeltrd 2509 . 2
27 coass 5380 . . 3
2815oveqd 6090 . . . . 5
2928adantr 452 . . . 4
30 simpl 444 . . . . 5
31263adant3r3 1164 . . . . 5
32 simpr3 965 . . . . 5
331, 2, 3, 4, 12erngmul 31504 . . . . 5
3430, 31, 32, 33syl12anc 1182 . . . 4
3515proplem3 13906 . . . . . 6
36223adantr3 1118 . . . . . 6
3735, 36eqtrd 2467 . . . . 5
3837coeq1d 5026 . . . 4
3929, 34, 383eqtrd 2471 . . 3
4015oveqd 6090 . . . . 5
4140adantr 452 . . . 4
42 simpr1 963 . . . . 5
4315proplem3 13906 . . . . . . 7
441, 2, 3, 4, 12erngmul 31504 . . . . . . . 8
45443adantr1 1116 . . . . . . 7
4643, 45eqtrd 2467 . . . . . 6
471, 3tendococl 31470 . . . . . . 7
48473adant3r1 1162 . . . . . 6
4946, 48eqeltrd 2509 . . . . 5
501, 2, 3, 4, 12erngmul 31504 . . . . 5
5130, 42, 49, 50syl12anc 1182 . . . 4
5246coeq2d 5027 . . . 4
5341, 51, 523eqtrd 2471 . . 3
5427, 39, 533eqtr4a 2493 . 2
551, 2, 3, 10tendodi1 31482 . . 3
5615oveqd 6090 . . . . 5
5756adantr 452 . . . 4
581, 2, 3, 10tendoplcl 31479 . . . . . 6
59583adant3r1 1162 . . . . 5
601, 2, 3, 4, 12erngmul 31504 . . . . 5
6130, 42, 59, 60syl12anc 1182 . . . 4
6257, 61eqtrd 2467 . . 3
6315proplem3 13906 . . . . 5
641, 2, 3, 4, 12erngmul 31504 . . . . . 6
65643adantr2 1117 . . . . 5
6663, 65eqtrd 2467 . . . 4
6737, 66oveq12d 6091 . . 3
6855, 62, 673eqtr4d 2477 . 2
691, 2, 3, 10tendodi2 31483 . . 3
7015oveqd 6090 . . . . 5
7170adantr 452 . . . 4
721, 2, 3, 10tendoplcl 31479 . . . . . 6
73723adant3r3 1164 . . . . 5
741, 2, 3, 4, 12erngmul 31504 . . . . 5
7530, 73, 32, 74syl12anc 1182 . . . 4
7671, 75eqtrd 2467 . . 3
7766, 46oveq12d 6091 . . 3
7869, 76, 773eqtr4d 2477 . 2
791, 2, 3tendoidcl 31467 . 2
8015oveqd 6090 . . . 4
82 simpl 444 . . . 4
8379adantr 452 . . . 4
84 simpr 448 . . . 4
851, 2, 3, 4, 12erngmul 31504 . . . 4
8682, 83, 84, 85syl12anc 1182 . . 3
871, 2, 3tendo1mul 31468 . . 3
8881, 86, 873eqtrd 2471 . 2
8915oveqd 6090 . . . 4