Metamath Proof Explorer


Theorem mdetfval1

Description: First substitution of an alternative determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by AV, 27-Dec-2018)

Ref Expression
Hypotheses mdetfval1.d D = N maDet R
mdetfval1.a A = N Mat R
mdetfval1.b B = Base A
mdetfval1.p P = Base SymGrp N
mdetfval1.y Y = ℤRHom R
mdetfval1.s S = pmSgn N
mdetfval1.t · ˙ = R
mdetfval1.u U = mulGrp R
Assertion mdetfval1 D = m B R p P Y S p · ˙ U x N p x m x

Proof

Step Hyp Ref Expression
1 mdetfval1.d D = N maDet R
2 mdetfval1.a A = N Mat R
3 mdetfval1.b B = Base A
4 mdetfval1.p P = Base SymGrp N
5 mdetfval1.y Y = ℤRHom R
6 mdetfval1.s S = pmSgn N
7 mdetfval1.t · ˙ = R
8 mdetfval1.u U = mulGrp R
9 1 2 3 4 5 6 7 8 mdetfval D = m B R p P Y S p · ˙ U x N p x m x
10 4 6 cofipsgn N Fin p P Y S p = Y S p
11 10 oveq1d N Fin p P Y S p · ˙ U x N p x m x = Y S p · ˙ U x N p x m x
12 11 mpteq2dva N Fin p P Y S p · ˙ U x N p x m x = p P Y S p · ˙ U x N p x m x
13 12 oveq2d N Fin R p P Y S p · ˙ U x N p x m x = R p P Y S p · ˙ U x N p x m x
14 13 mpteq2dv N Fin m B R p P Y S p · ˙ U x N p x m x = m B R p P Y S p · ˙ U x N p x m x
15 9 14 syl5eq N Fin D = m B R p P Y S p · ˙ U x N p x m x
16 df-nel N Fin ¬ N Fin
17 1 nfimdetndef N Fin D =
18 2 fveq2i Base A = Base N Mat R
19 3 18 eqtri B = Base N Mat R
20 16 biimpi N Fin ¬ N Fin
21 20 intnanrd N Fin ¬ N Fin R V
22 matbas0 ¬ N Fin R V Base N Mat R =
23 21 22 syl N Fin Base N Mat R =
24 19 23 syl5eq N Fin B =
25 24 mpteq1d N Fin m B R p P Y S p · ˙ U x N p x m x = m R p P Y S p · ˙ U x N p x m x
26 mpt0 m R p P Y S p · ˙ U x N p x m x =
27 25 26 eqtrdi N Fin m B R p P Y S p · ˙ U x N p x m x =
28 17 27 eqtr4d N Fin D = m B R p P Y S p · ˙ U x N p x m x
29 16 28 sylbir ¬ N Fin D = m B R p P Y S p · ˙ U x N p x m x
30 15 29 pm2.61i D = m B R p P Y S p · ˙ U x N p x m x