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

Theorem erngdvlem3 34569
 Description: Lemma for eringring 34571. (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 2453 . . . 4
61, 2, 3, 4, 5erngbase 34380 . . 3
76eqcomd 2459 . 2
8 eqid 2453 . . . 4
91, 2, 3, 4, 8erngfplus 34381 . . 3
10 erngdv.p . . 3
119, 10syl6reqr 2506 . 2
12 eqid 2453 . . . 4
131, 2, 3, 4, 12erngfmul 34384 . . 3
14 erngrnglem.m . . 3
1513, 14syl6reqr 2506 . 2
16 erngdv.b . . 3
17 erngdv.o . . 3
18 erngdv.i . . 3
191, 4, 16, 2, 3, 10, 17, 18erngdvlem1 34567 . 2
2015oveqd 6312 . . . . 5
21203ad2ant1 1030 . . . 4
221, 2, 3, 4, 12erngmul 34385 . . . . 5
23223impb 1205 . . . 4
2421, 23eqtrd 2487 . . 3
251, 3tendococl 34351 . . 3
2624, 25eqeltrd 2531 . 2
27 coass 5357 . . 3
2815oveqd 6312 . . . . 5
2928adantr 467 . . . 4
30 simpl 459 . . . . 5
31263adant3r3 1220 . . . . 5
32 simpr3 1017 . . . . 5
331, 2, 3, 4, 12erngmul 34385 . . . . 5
3430, 31, 32, 33syl12anc 1267 . . . 4
3515oveqdr 6319 . . . . . 6
36223adantr3 1170 . . . . . 6
3735, 36eqtrd 2487 . . . . 5
3837coeq1d 4999 . . . 4
3929, 34, 383eqtrd 2491 . . 3
4015oveqd 6312 . . . . 5
4140adantr 467 . . . 4
42 simpr1 1015 . . . . 5
4315oveqdr 6319 . . . . . . 7
441, 2, 3, 4, 12erngmul 34385 . . . . . . . 8
45443adantr1 1168 . . . . . . 7
4643, 45eqtrd 2487 . . . . . 6
471, 3tendococl 34351 . . . . . . 7
48473adant3r1 1218 . . . . . 6
4946, 48eqeltrd 2531 . . . . 5
501, 2, 3, 4, 12erngmul 34385 . . . . 5
5130, 42, 49, 50syl12anc 1267 . . . 4
5246coeq2d 5000 . . . 4
5341, 51, 523eqtrd 2491 . . 3
5427, 39, 533eqtr4a 2513 . 2
551, 2, 3, 10tendodi1 34363 . . 3
5615oveqd 6312 . . . . 5
5756adantr 467 . . . 4
581, 2, 3, 10tendoplcl 34360 . . . . . 6
59583adant3r1 1218 . . . . 5
601, 2, 3, 4, 12erngmul 34385 . . . . 5
6130, 42, 59, 60syl12anc 1267 . . . 4
6257, 61eqtrd 2487 . . 3
6315oveqdr 6319 . . . . 5
641, 2, 3, 4, 12erngmul 34385 . . . . . 6
65643adantr2 1169 . . . . 5
6663, 65eqtrd 2487 . . . 4
6737, 66oveq12d 6313 . . 3
6855, 62, 673eqtr4d 2497 . 2
691, 2, 3, 10tendodi2 34364 . . 3
7015oveqd 6312 . . . . 5
7170adantr 467 . . . 4
721, 2, 3, 10tendoplcl 34360 . . . . . 6
73723adant3r3 1220 . . . . 5
741, 2, 3, 4, 12erngmul 34385 . . . . 5
7530, 73, 32, 74syl12anc 1267 . . . 4
7671, 75eqtrd 2487 . . 3
7766, 46oveq12d 6313 . . 3
7869, 76, 773eqtr4d 2497 . 2
791, 2, 3tendoidcl 34348 . 2
8015oveqd 6312 . . . 4
82 simpl 459 . . . 4
8379adantr 467 . . . 4
84 simpr 463 . . . 4
851, 2, 3, 4, 12erngmul 34385 . . . 4
8682, 83, 84, 85syl12anc 1267 . . 3
871, 2, 3tendo1mul 34349 . . 3
8881, 86, 873eqtrd 2491 . 2
8915oveqd 6312 . . . 4