Step | Hyp | Ref
| Expression |
1 | | mdetdiag.d |
. . . 4
maDet |
2 | | mdetdiag.a |
. . . 4
Mat |
3 | | mdetdiag.b |
. . . 4
|
4 | | eqid 2622 |
. . . 4
|
5 | | eqid 2622 |
. . . 4
RHom RHom |
6 | | eqid 2622 |
. . . 4
pmSgn pmSgn |
7 | | eqid 2622 |
. . . 4
|
8 | | eqid 2622 |
. . . 4
mulGrp mulGrp |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib 20393 |
. . 3
g RHom pmSgnmulGrp g |
10 | 9 | 3ad2ant3 1084 |
. 2
g RHom pmSgnmulGrp g |
11 | | fveq2 6191 |
. . . . . . . . 9
|
12 | 11 | fveq2d 6195 |
. . . . . . . 8
|
13 | 12 | adantr 481 |
. . . . . . 7
|
14 | 13 | 3ad2ant2 1083 |
. . . . . 6
|
15 | | simp2r 1088 |
. . . . . . 7
|
16 | | eqid 2622 |
. . . . . . . 8
|
17 | | eqid 2622 |
. . . . . . . 8
|
18 | | eqid 2622 |
. . . . . . . 8
|
19 | 16, 17, 18 | symg1bas 17816 |
. . . . . . 7
|
20 | 15, 19 | syl 17 |
. . . . . 6
|
21 | 14, 20 | eqtrd 2656 |
. . . . 5
|
22 | 21 | mpteq1d 4738 |
. . . 4
RHom pmSgnmulGrp g RHom pmSgnmulGrp g |
23 | | snex 4908 |
. . . . . 6
|
24 | 23 | a1i 11 |
. . . . 5
|
25 | | ovex 6678 |
. . . . 5
RHom pmSgn mulGrp g |
26 | | fveq2 6191 |
. . . . . . . 8
RHom pmSgn RHom pmSgn |
27 | | fveq1 6190 |
. . . . . . . . . . 11
|
28 | 27 | oveq1d 6665 |
. . . . . . . . . 10
|
29 | 28 | mpteq2dv 4745 |
. . . . . . . . 9
|
30 | 29 | oveq2d 6666 |
. . . . . . . 8
mulGrp g mulGrp g |
31 | 26, 30 | oveq12d 6668 |
. . . . . . 7
RHom pmSgnmulGrp g RHom pmSgn mulGrp g |
32 | 31 | fmptsng 6434 |
. . . . . 6
RHom pmSgn mulGrp g RHom pmSgn mulGrp g
RHom pmSgnmulGrp g |
33 | 32 | eqcomd 2628 |
. . . . 5
RHom pmSgn mulGrp g RHom pmSgnmulGrp g RHom pmSgn mulGrp g |
34 | 24, 25, 33 | sylancl 694 |
. . . 4
RHom pmSgnmulGrp g RHom pmSgn mulGrp g |
35 | | eqid 2622 |
. . . . . . . . . . . . 13
|
36 | | eqid 2622 |
. . . . . . . . . . . . 13
|
37 | 35, 4, 36, 6 | psgnfn 17921 |
. . . . . . . . . . . 12
pmSgn
|
38 | 19 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
39 | 13, 38 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
|
41 | | rabeq 3192 |
. . . . . . . . . . . . . . 15
|
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
|
43 | | difeq1 3721 |
. . . . . . . . . . . . . . . . . 18
|
44 | 43 | dmeqd 5326 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
46 | 45 | rabsnif 4258 |
. . . . . . . . . . . . . . 15
|
47 | 46 | a1i 11 |
. . . . . . . . . . . . . 14
|
48 | | restidsing 5458 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | | xpsng 6406 |
. . . . . . . . . . . . . . . . . . . . 21
|
50 | 49 | anidms 677 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | 48, 50 | syl5req 2669 |
. . . . . . . . . . . . . . . . . . 19
|
52 | | fnsng 5938 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 52 | anidms 677 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | | fnnfpeq0 6444 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 51, 55 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
57 | | 0fin 8188 |
. . . . . . . . . . . . . . . . . 18
|
58 | 56, 57 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
60 | 59 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
|
61 | 60 | iftrued 4094 |
. . . . . . . . . . . . . 14
|
62 | 42, 47, 61 | 3eqtrrd 2661 |
. . . . . . . . . . . . 13
|
63 | 62 | fneq2d 5982 |
. . . . . . . . . . . 12
pmSgn
pmSgn |
64 | 37, 63 | mpbiri 248 |
. . . . . . . . . . 11
pmSgn |
65 | 23 | snid 4208 |
. . . . . . . . . . 11
|
66 | | fvco2 6273 |
. . . . . . . . . . 11
pmSgn
RHom pmSgn RHompmSgn |
67 | 64, 65, 66 | sylancl 694 |
. . . . . . . . . 10
RHom pmSgn RHompmSgn |
68 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
pmSgn pmSgn |
69 | 68 | adantr 481 |
. . . . . . . . . . . . . 14
pmSgn pmSgn |
70 | 69 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
pmSgn pmSgn |
71 | 70 | fveq1d 6193 |
. . . . . . . . . . . 12
pmSgn pmSgn |
72 | | snidg 4206 |
. . . . . . . . . . . . . . . . . 18
|
73 | 23, 72 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
|
74 | 73, 19 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | ancli 574 |
. . . . . . . . . . . . . . 15
|
76 | 75 | adantl 482 |
. . . . . . . . . . . . . 14
|
77 | 76 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
|
78 | | eqid 2622 |
. . . . . . . . . . . . . 14
pmSgn pmSgn |
79 | 18, 16, 17, 78 | psgnsn 17940 |
. . . . . . . . . . . . 13
pmSgn |
80 | 77, 79 | syl 17 |
. . . . . . . . . . . 12
pmSgn |
81 | 71, 80 | eqtrd 2656 |
. . . . . . . . . . 11
pmSgn |
82 | 81 | fveq2d 6195 |
. . . . . . . . . 10
RHompmSgn RHom |
83 | | crngring 18558 |
. . . . . . . . . . . 12
|
84 | 83 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
85 | | eqid 2622 |
. . . . . . . . . . . 12
|
86 | 5, 85 | zrh1 19861 |
. . . . . . . . . . 11
RHom |
87 | 84, 86 | syl 17 |
. . . . . . . . . 10
RHom |
88 | 67, 82, 87 | 3eqtrd 2660 |
. . . . . . . . 9
RHom pmSgn |
89 | | simp2l 1087 |
. . . . . . . . . . . 12
|
90 | 89 | mpteq1d 4738 |
. . . . . . . . . . 11
|
91 | 90 | oveq2d 6666 |
. . . . . . . . . 10
mulGrp g mulGrp g |
92 | 8 | ringmgp 18553 |
. . . . . . . . . . . . 13
mulGrp |
93 | 83, 92 | syl 17 |
. . . . . . . . . . . 12
mulGrp |
94 | 93 | 3ad2ant1 1082 |
. . . . . . . . . . 11
mulGrp |
95 | | snidg 4206 |
. . . . . . . . . . . . . . . . 17
|
96 | 95 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
97 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
98 | 97 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
99 | 96, 98 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
100 | 3 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
|
101 | 100 | biimpi 206 |
. . . . . . . . . . . . . . 15
|
102 | | simpl 473 |
. . . . . . . . . . . . . . . 16
|
103 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
104 | 102, 102,
103 | 3jca 1242 |
. . . . . . . . . . . . . . 15
|
105 | 99, 101, 104 | syl2an 494 |
. . . . . . . . . . . . . 14
|
106 | 105 | 3adant1 1079 |
. . . . . . . . . . . . 13
|
107 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
108 | 2, 107 | matecl 20231 |
. . . . . . . . . . . . 13
|
109 | 106, 108 | syl 17 |
. . . . . . . . . . . 12
|
110 | 8, 107 | mgpbas 18495 |
. . . . . . . . . . . 12
mulGrp |
111 | 109, 110 | syl6eleq 2711 |
. . . . . . . . . . 11
mulGrp |
112 | | eqid 2622 |
. . . . . . . . . . . 12
mulGrp mulGrp |
113 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
114 | | eqvisset 3211 |
. . . . . . . . . . . . . . 15
|
115 | | fvsng 6447 |
. . . . . . . . . . . . . . 15
|
116 | 114, 114,
115 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
117 | 113, 116 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
118 | | id 22 |
. . . . . . . . . . . . 13
|
119 | 117, 118 | oveq12d 6668 |
. . . . . . . . . . . 12
|
120 | 112, 119 | gsumsn 18354 |
. . . . . . . . . . 11
mulGrp mulGrp mulGrp g |
121 | 94, 15, 111, 120 | syl3anc 1326 |
. . . . . . . . . 10
mulGrp g |
122 | 91, 121 | eqtrd 2656 |
. . . . . . . . 9
mulGrp g |
123 | 88, 122 | oveq12d 6668 |
. . . . . . . 8
RHom pmSgn mulGrp g |
124 | 99 | 3ad2ant2 1083 |
. . . . . . . . . 10
|
125 | 101 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
126 | 124, 124,
125, 108 | syl3anc 1326 |
. . . . . . . . 9
|
127 | 107, 7, 85 | ringlidm 18571 |
. . . . . . . . 9
|
128 | 84, 126, 127 | syl2anc 693 |
. . . . . . . 8
|
129 | 123, 128 | eqtrd 2656 |
. . . . . . 7
RHom pmSgn mulGrp g |
130 | 129 | opeq2d 4409 |
. . . . . 6
RHom pmSgn mulGrp g
|
131 | 130 | sneqd 4189 |
. . . . 5
RHom pmSgn mulGrp g
|
132 | | ovex 6678 |
. . . . . 6
|
133 | | eqidd 2623 |
. . . . . . 7
|
134 | 133 | fmptsng 6434 |
. . . . . 6
|
135 | 24, 132, 134 | sylancl 694 |
. . . . 5
|
136 | 131, 135 | eqtrd 2656 |
. . . 4
RHom pmSgn mulGrp g
|
137 | 22, 34, 136 | 3eqtrd 2660 |
. . 3
RHom pmSgnmulGrp g |
138 | 137 | oveq2d 6666 |
. 2
g RHom pmSgnmulGrp g g |
139 | | ringmnd 18556 |
. . . . 5
|
140 | 83, 139 | syl 17 |
. . . 4
|
141 | 140 | 3ad2ant1 1082 |
. . 3
|
142 | 107, 133 | gsumsn 18354 |
. . 3
g |
143 | 141, 24, 126, 142 | syl3anc 1326 |
. 2
g |
144 | 10, 138, 143 | 3eqtrd 2660 |
1
|