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 ) ) ) ) ) ) )