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

Theorem erngdvlem4-rN 33998
 Description: Lemma for erngdv 33992. (Contributed by NM, 11-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
edlemk6.j-r
edlemk6.m-r
edlemk6.r-r
edlemk6.p-r
edlemk6.z-r
edlemk6.y-r
edlemk6.x-r
edlemk6.u-r
Assertion
Ref Expression
erngdvlem4-rN
Distinct variable groups:   ,   ,   ,,,   ,,,,   ,,   ,   ,,,,   ,,,,   ,   ,,,   ,,,   ,   ,,,   ,,,   ,,   ,   ,,   ,,,   ,,,   ,,   ,,   ,   ,   ,,   ,,,,
Allowed substitution hints:   (,)   (,,,,,)   (,,,)   (,,,)   (,,,)   ()   (,,,,,,)   (,,,)   (,)   (,,,,,,)   (,,,)   ()   (,,,,,)   (,,,)   (,,,,,)   ()   (,,,,,,)   (,,,,,)   (,,,,,)

Proof of Theorem erngdvlem4-rN
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ernggrp.h-r . . . . 5
2 ernggrplem.t-r . . . . 5
3 ernggrplem.e-r . . . . 5
4 ernggrp.d-r . . . . 5
5 eqid 2402 . . . . 5
61, 2, 3, 4, 5erngbase-rN 33808 . . . 4
76eqcomd 2410 . . 3
9 eqid 2402 . . . . 5
101, 2, 3, 4, 9erngfmul-rN 33812 . . . 4
11 erngrnglem.m-r . . . 4
1210, 11syl6reqr 2462 . . 3
14 ernggrplem.b-r . . . . . . 7
15 ernggrplem.o-r . . . . . . 7
1614, 1, 2, 3, 15tendo0cl 33789 . . . . . 6
1716, 6eleqtrrd 2493 . . . . 5
18 eqid 2402 . . . . . . . . 9
191, 2, 3, 4, 18erngfplus-rN 33809 . . . . . . . 8
20 ernggrplem.p-r . . . . . . . 8
2119, 20syl6reqr 2462 . . . . . . 7
2221oveqd 6294 . . . . . 6
2314, 1, 2, 3, 15, 20tendo0pl 33790 . . . . . . 7
2416, 23mpdan 666 . . . . . 6
2522, 24eqtr3d 2445 . . . . 5
26 ernggrplem.i-r . . . . . . 7
271, 4, 14, 2, 3, 20, 15, 26erngdvlem1-rN 33995 . . . . . 6
28 eqid 2402 . . . . . . 7
295, 18, 28isgrpid2 16408 . . . . . 6
3027, 29syl 17 . . . . 5
3117, 25, 30mpbi2and 922 . . . 4
3231eqcomd 2410 . . 3
341, 2, 3tendoidcl 33768 . . . . . 6
3534, 6eleqtrrd 2493 . . . . 5
366eleq2d 2472 . . . . . . 7
37 simpl 455 . . . . . . . . . . 11
3834adantr 463 . . . . . . . . . . 11
39 simpr 459 . . . . . . . . . . 11
401, 2, 3, 4, 9erngmul-rN 33813 . . . . . . . . . . 11
4137, 38, 39, 40syl12anc 1228 . . . . . . . . . 10
421, 2, 3tendo1mulr 33770 . . . . . . . . . 10
4341, 42eqtrd 2443 . . . . . . . . 9
441, 2, 3, 4, 9erngmul-rN 33813 . . . . . . . . . . 11
4537, 39, 38, 44syl12anc 1228 . . . . . . . . . 10
461, 2, 3tendo1mul 33769 . . . . . . . . . 10
4745, 46eqtrd 2443 . . . . . . . . 9
4843, 47jca 530 . . . . . . . 8
4948ex 432 . . . . . . 7
5036, 49sylbid 215 . . . . . 6
5150ralrimiv 2815 . . . . 5
521, 4, 14, 2, 3, 20, 15, 26, 11erngdvlem3-rN 33997 . . . . . 6
53 eqid 2402 . . . . . . 7
545, 9, 53isringid 17542 . . . . . 6
5552, 54syl 17 . . . . 5
5635, 51, 55mpbi2and 922 . . . 4
5756eqcomd 2410 . . 3
60 simp1l 1021 . . . . 5
6112oveqd 6294 . . . . 5
6260, 61syl 17 . . . 4
63 simp2l 1023 . . . . 5
64 simp3l 1025 . . . . 5
651, 2, 3, 4, 9erngmul-rN 33813 . . . . 5
6660, 63, 64, 65syl12anc 1228 . . . 4
6762, 66eqtrd 2443 . . 3
68 simp3 999 . . . 4
69 simp2 998 . . . 4
7014, 1, 2, 3, 15tendoconid 33828 . . . 4
7160, 68, 69, 70syl3anc 1230 . . 3
7267, 71eqnetrd 2696 . 2
7314, 1, 2, 3, 15tendo1ne0 33827 . . 3
75 simpll 752 . . 3
76 simplrl 762 . . 3
77 simpr 459 . . 3
78 edlemk6.j-r . . . . 5
79 edlemk6.m-r . . . . 5
80 edlemk6.r-r . . . . 5
81 edlemk6.p-r . . . . 5
82 edlemk6.z-r . . . . 5
83 edlemk6.y-r . . . . 5
84 edlemk6.x-r . . . . 5
85 edlemk6.u-r . . . . 5
8614, 78, 79, 1, 2, 80, 81, 82, 83, 84, 85, 3, 15cdleml6 33980 . . . 4
8786simpld 457 . . 3
8875, 76, 77, 87syl3anc 1230 . 2
8914, 78, 79, 1, 2, 80, 81, 82, 83, 84, 85, 3, 15cdleml9 33983 . . 3
90893expa 1197 . 2
9112oveqd 6294 . . . 4