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

Theorem erngdvlem4 30998
 Description: Lemma for erngdv 31000. (Contributed by NM, 11-Aug-2013.)
Hypotheses
Ref Expression
ernggrp.h
ernggrp.d
erngdv.b
erngdv.t
erngdv.e
erngdv.p
erngdv.o
erngdv.i
erngrnglem.m
edlemk6.j
edlemk6.m
edlemk6.r
edlemk6.p
edlemk6.z
edlemk6.y
edlemk6.x
edlemk6.u
Assertion
Ref Expression
erngdvlem4
Distinct variable groups:   ,   ,   ,,,   ,,,,   ,,   ,   ,,,,   ,,,,   ,   ,,,   ,,,   ,   ,,,   ,,,   ,,   ,   ,,   ,,,   ,,,   ,,   ,,   ,   ,   ,,   ,,,,
Allowed substitution hints:   (,)   (,,,,,)   (,,,)   (,,,,,)   (,,,)   (,,,)   ()   (,,,,,,)   (,,,)   (,)   (,,,,,,)   (,,,)   ()   (,,,)   ()   (,,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)

Proof of Theorem erngdvlem4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ernggrp.h . . . . 5
2 erngdv.t . . . . 5
3 erngdv.e . . . . 5
4 ernggrp.d . . . . 5
5 eqid 2316 . . . . 5
61, 2, 3, 4, 5erngbase 30808 . . . 4
76eqcomd 2321 . . 3
9 eqid 2316 . . . . 5
101, 2, 3, 4, 9erngfmul 30812 . . . 4
11 erngrnglem.m . . . 4
1210, 11syl6reqr 2367 . . 3
14 erngdv.b . . . . . . 7
15 erngdv.o . . . . . . 7
1614, 1, 2, 3, 15tendo0cl 30797 . . . . . 6
1716, 6eleqtrrd 2393 . . . . 5
18 eqid 2316 . . . . . . . . 9
191, 2, 3, 4, 18erngfplus 30809 . . . . . . . 8
20 erngdv.p . . . . . . . 8
2119, 20syl6reqr 2367 . . . . . . 7
2221oveqd 5917 . . . . . 6
2314, 1, 2, 3, 15, 20tendo0pl 30798 . . . . . . 7
2416, 23mpdan 649 . . . . . 6
2522, 24eqtr3d 2350 . . . . 5
26 erngdv.i . . . . . . 7
271, 4, 14, 2, 3, 20, 15, 26erngdvlem1 30995 . . . . . 6
28 eqid 2316 . . . . . . 7
295, 18, 28isgrpid2 14567 . . . . . 6
3027, 29syl 15 . . . . 5
3117, 25, 30mpbi2and 887 . . . 4
3231eqcomd 2321 . . 3
341, 4, 14, 2, 3, 20, 15, 26, 11erngdvlem3 30997 . . . . 5
351, 2, 3, 4, 34erng1lem 30994 . . . 4
3635eqcomd 2321 . . 3
39 simp1l 979 . . . . 5
4012oveqd 5917 . . . . 5
4139, 40syl 15 . . . 4
42 simp2l 981 . . . . 5
43 simp3l 983 . . . . 5
441, 2, 3, 4, 9erngmul 30813 . . . . 5
4539, 42, 43, 44syl12anc 1180 . . . 4
4641, 45eqtrd 2348 . . 3
4714, 1, 2, 3, 15tendoconid 30836 . . . 4
4946, 48eqnetrd 2497 . 2
5014, 1, 2, 3, 15tendo1ne0 30835 . . 3
52 simpll 730 . . 3
53 simplrl 736 . . 3
54 simpr 447 . . 3
55 edlemk6.j . . . . 5
56 edlemk6.m . . . . 5
57 edlemk6.r . . . . 5
58 edlemk6.p . . . . 5
59 edlemk6.z . . . . 5
60 edlemk6.y . . . . 5
61 edlemk6.x . . . . 5
62 edlemk6.u . . . . 5
6314, 55, 56, 1, 2, 57, 58, 59, 60, 61, 62, 3, 15cdleml6 30988 . . . 4
6463simpld 445 . . 3
6552, 53, 54, 64syl3anc 1182 . 2
6614, 55, 56, 1, 2, 57, 58, 59, 60, 61, 62, 3, 15cdleml9 30991 . . 3
67663expa 1151 . 2
6812oveqd 5917 . . . 4