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 = ( ZRHom ` R )
mdetfval1.s
|- S = ( pmSgn ` N )
mdetfval1.t
|- .x. = ( .r ` R )
mdetfval1.u
|- U = ( mulGrp ` R )
Assertion mdetfval1
|- D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. 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 = ( ZRHom ` R )
6 mdetfval1.s
 |-  S = ( pmSgn ` N )
7 mdetfval1.t
 |-  .x. = ( .r ` R )
8 mdetfval1.u
 |-  U = ( mulGrp ` R )
9 1 2 3 4 5 6 7 8 mdetfval
 |-  D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) )
10 4 6 cofipsgn
 |-  ( ( N e. Fin /\ p e. P ) -> ( ( Y o. S ) ` p ) = ( Y ` ( S ` p ) ) )
11 10 oveq1d
 |-  ( ( N e. Fin /\ p e. P ) -> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) = ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) )
12 11 mpteq2dva
 |-  ( N e. Fin -> ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) = ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) )
13 12 oveq2d
 |-  ( N e. Fin -> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) = ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) )
14 13 mpteq2dv
 |-  ( N e. Fin -> ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
15 9 14 syl5eq
 |-  ( N e. Fin -> D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
16 df-nel
 |-  ( N e/ Fin <-> -. N e. Fin )
17 1 nfimdetndef
 |-  ( N e/ Fin -> D = (/) )
18 2 fveq2i
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
19 3 18 eqtri
 |-  B = ( Base ` ( N Mat R ) )
20 16 biimpi
 |-  ( N e/ Fin -> -. N e. Fin )
21 20 intnanrd
 |-  ( N e/ Fin -> -. ( N e. Fin /\ R e. _V ) )
22 matbas0
 |-  ( -. ( N e. Fin /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) )
23 21 22 syl
 |-  ( N e/ Fin -> ( Base ` ( N Mat R ) ) = (/) )
24 19 23 syl5eq
 |-  ( N e/ Fin -> B = (/) )
25 24 mpteq1d
 |-  ( N e/ Fin -> ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. (/) |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
26 mpt0
 |-  ( m e. (/) |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/)
27 25 26 eqtrdi
 |-  ( N e/ Fin -> ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/) )
28 17 27 eqtr4d
 |-  ( N e/ Fin -> D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
29 16 28 sylbir
 |-  ( -. N e. Fin -> D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
30 15 29 pm2.61i
 |-  D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) )