Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  m1detdiag Structured version   Unicode version

Theorem m1detdiag 18859
 Description: The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.)
Hypotheses
Ref Expression
mdetdiag.a Mat
mdetdiag.b
Assertion
Ref Expression
m1detdiag

Proof of Theorem m1detdiag
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetdiag.d . . . 4 maDet
2 mdetdiag.a . . . 4 Mat
3 mdetdiag.b . . . 4
4 eqid 2460 . . . 4
5 eqid 2460 . . . 4 RHom RHom
6 eqid 2460 . . . 4 pmSgn pmSgn
7 eqid 2460 . . . 4
8 eqid 2460 . . . 4 mulGrp mulGrp
91, 2, 3, 4, 5, 6, 7, 8mdetleib 18849 . . 3 g RHom pmSgnmulGrp g
1093ad2ant3 1014 . 2 g RHom pmSgnmulGrp g
11 fveq2 5857 . . . . . . . . 9
1211fveq2d 5861 . . . . . . . 8
1312adantr 465 . . . . . . 7
14133ad2ant2 1013 . . . . . 6
15 simp2r 1018 . . . . . . 7
16 eqid 2460 . . . . . . . 8
17 eqid 2460 . . . . . . . 8
18 eqid 2460 . . . . . . . 8
1916, 17, 18symg1bas 16209 . . . . . . 7
2015, 19syl 16 . . . . . 6
2114, 20eqtrd 2501 . . . . 5
2221mpteq1d 4521 . . . 4 RHom pmSgnmulGrp g RHom pmSgnmulGrp g
23 snex 4681 . . . . . 6
2423a1i 11 . . . . 5
25 ovex 6300 . . . . 5 RHom pmSgn mulGrp g
26 fveq2 5857 . . . . . . . 8 RHom pmSgn RHom pmSgn
27 fveq1 5856 . . . . . . . . . . 11
2827oveq1d 6290 . . . . . . . . . 10
2928mpteq2dv 4527 . . . . . . . . 9
3029oveq2d 6291 . . . . . . . 8 mulGrp g mulGrp g
3126, 30oveq12d 6293 . . . . . . 7 RHom pmSgnmulGrp g RHom pmSgn mulGrp g
3231fmptsng 6073 . . . . . 6 RHom pmSgn mulGrp g RHom pmSgn mulGrp g RHom pmSgnmulGrp g
3332eqcomd 2468 . . . . 5 RHom pmSgn mulGrp g RHom pmSgnmulGrp g RHom pmSgn mulGrp g
3424, 25, 33sylancl 662 . . . 4 RHom pmSgnmulGrp g RHom pmSgn mulGrp g
35 eqid 2460 . . . . . . . . . . . . 13
36 eqid 2460 . . . . . . . . . . . . 13
3735, 4, 36, 6psgnfn 16315 . . . . . . . . . . . 12 pmSgn
3819adantl 466 . . . . . . . . . . . . . . . . 17
3913, 38eqtrd 2501 . . . . . . . . . . . . . . . 16
40393ad2ant2 1013 . . . . . . . . . . . . . . 15
41 rabeq 3100 . . . . . . . . . . . . . . 15
4240, 41syl 16 . . . . . . . . . . . . . 14
43 difeq1 3608 . . . . . . . . . . . . . . . . . 18
4443dmeqd 5196 . . . . . . . . . . . . . . . . 17
4544eleq1d 2529 . . . . . . . . . . . . . . . 16
4645rabsnif 4089 . . . . . . . . . . . . . . 15
4746a1i 11 . . . . . . . . . . . . . 14
48 restidsing 5321 . . . . . . . . . . . . . . . . . . . 20
49 xpsng 6053 . . . . . . . . . . . . . . . . . . . . 21
5049anidms 645 . . . . . . . . . . . . . . . . . . . 20
5148, 50syl5req 2514 . . . . . . . . . . . . . . . . . . 19
52 fnsng 5626 . . . . . . . . . . . . . . . . . . . . 21
5352anidms 645 . . . . . . . . . . . . . . . . . . . 20
54 fnnfpeq0 6083 . . . . . . . . . . . . . . . . . . . 20
5553, 54syl 16 . . . . . . . . . . . . . . . . . . 19
5651, 55mpbird 232 . . . . . . . . . . . . . . . . . 18
57 0fin 7737 . . . . . . . . . . . . . . . . . 18
5856, 57syl6eqel 2556 . . . . . . . . . . . . . . . . 17
5958adantl 466 . . . . . . . . . . . . . . . 16
60593ad2ant2 1013 . . . . . . . . . . . . . . 15
61 iftrue 3938 . . . . . . . . . . . . . . 15
6260, 61syl 16 . . . . . . . . . . . . . 14
6342, 47, 623eqtrrd 2506 . . . . . . . . . . . . 13
6463fneq2d 5663 . . . . . . . . . . . 12 pmSgn pmSgn
6537, 64mpbiri 233 . . . . . . . . . . 11 pmSgn
6623snid 4048 . . . . . . . . . . 11
67 fvco2 5933 . . . . . . . . . . 11 pmSgn RHom pmSgn RHompmSgn
6865, 66, 67sylancl 662 . . . . . . . . . 10 RHom pmSgn RHompmSgn
69 fveq2 5857 . . . . . . . . . . . . . . 15 pmSgn pmSgn
7069adantr 465 . . . . . . . . . . . . . 14 pmSgn pmSgn
71703ad2ant2 1013 . . . . . . . . . . . . 13 pmSgn pmSgn
7271fveq1d 5859 . . . . . . . . . . . 12 pmSgn pmSgn
73 snidg 4046 . . . . . . . . . . . . . . . . . 18
7423, 73mp1i 12 . . . . . . . . . . . . . . . . 17
7574, 19eleqtrrd 2551 . . . . . . . . . . . . . . . 16
7675ancli 551 . . . . . . . . . . . . . . 15
7776adantl 466 . . . . . . . . . . . . . 14
78773ad2ant2 1013 . . . . . . . . . . . . 13
79 eqid 2460 . . . . . . . . . . . . . 14 pmSgn pmSgn
8018, 16, 17, 79psgnsn 16334 . . . . . . . . . . . . 13 pmSgn
8178, 80syl 16 . . . . . . . . . . . 12 pmSgn
8272, 81eqtrd 2501 . . . . . . . . . . 11 pmSgn
8382fveq2d 5861 . . . . . . . . . 10 RHompmSgn RHom
84 crngrng 16989 . . . . . . . . . . . 12
85843ad2ant1 1012 . . . . . . . . . . 11
86 eqid 2460 . . . . . . . . . . . 12
875, 86zrh1 18310 . . . . . . . . . . 11 RHom
8885, 87syl 16 . . . . . . . . . 10 RHom
8968, 83, 883eqtrd 2505 . . . . . . . . 9 RHom pmSgn
90 simp2l 1017 . . . . . . . . . . . 12
9190mpteq1d 4521 . . . . . . . . . . 11
9291oveq2d 6291 . . . . . . . . . 10 mulGrp g mulGrp g
938rngmgp 16985 . . . . . . . . . . . . 13 mulGrp
9484, 93syl 16 . . . . . . . . . . . 12 mulGrp
95943ad2ant1 1012 . . . . . . . . . . 11 mulGrp
96 snidg 4046 . . . . . . . . . . . . . . . . 17
9796adantl 466 . . . . . . . . . . . . . . . 16
98 eleq2 2533 . . . . . . . . . . . . . . . . 17
9998adantr 465 . . . . . . . . . . . . . . . 16
10097, 99mpbird 232 . . . . . . . . . . . . . . 15
1013eleq2i 2538 . . . . . . . . . . . . . . . 16
102101biimpi 194 . . . . . . . . . . . . . . 15
103 simpl 457 . . . . . . . . . . . . . . . 16
104 simpr 461 . . . . . . . . . . . . . . . 16
105103, 103, 1043jca 1171 . . . . . . . . . . . . . . 15
106100, 102, 105syl2an 477 . . . . . . . . . . . . . 14
1071063adant1 1009 . . . . . . . . . . . . 13
108 eqid 2460 . . . . . . . . . . . . . 14
1092, 108matecl 18687 . . . . . . . . . . . . 13
110107, 109syl 16 . . . . . . . . . . . 12
1118, 108mgpbas 16930 . . . . . . . . . . . 12 mulGrp
112110, 111syl6eleq 2558 . . . . . . . . . . 11 mulGrp
113 eqid 2460 . . . . . . . . . . . 12 mulGrp mulGrp
114 fveq2 5857 . . . . . . . . . . . . . 14
115 eqvisset 3114 . . . . . . . . . . . . . . 15
116 fvsng 6086 . . . . . . . . . . . . . . 15
117115, 115, 116syl2anc 661 . . . . . . . . . . . . . 14
118114, 117eqtrd 2501 . . . . . . . . . . . . 13
119 id 22 . . . . . . . . . . . . 13
120118, 119oveq12d 6293 . . . . . . . . . . . 12
121113, 120gsumsn 16765 . . . . . . . . . . 11 mulGrp mulGrp mulGrp g
12295, 15, 112, 121syl3anc 1223 . . . . . . . . . 10 mulGrp g
12392, 122eqtrd 2501 . . . . . . . . 9 mulGrp g
12489, 123oveq12d 6293 . . . . . . . 8 RHom pmSgn mulGrp g
1251003ad2ant2 1013 . . . . . . . . . 10
1261023ad2ant3 1014 . . . . . . . . . 10
127125, 125, 126, 109syl3anc 1223 . . . . . . . . 9
128108, 7, 86rnglidm 17002 . . . . . . . . 9
12985, 127, 128syl2anc 661 . . . . . . . 8
130124, 129eqtrd 2501 . . . . . . 7 RHom pmSgn mulGrp g
131130opeq2d 4213 . . . . . 6 RHom pmSgn mulGrp g
132131sneqd 4032 . . . . 5 RHom pmSgn mulGrp g
133 ovex 6300 . . . . . 6
134 eqidd 2461 . . . . . . 7
135134fmptsng 6073 . . . . . 6
13624, 133, 135sylancl 662 . . . . 5
137132, 136eqtrd 2501 . . . 4 RHom pmSgn mulGrp g
13822, 34, 1373eqtrd 2505 . . 3 RHom pmSgnmulGrp g
139138oveq2d 6291 . 2 g RHom pmSgnmulGrp g g
140 rngmnd 16988 . . . . 5
14184, 140syl 16 . . . 4