Metamath Proof Explorer

Theorem nfimdetndef

Description: The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018)

Ref Expression
Hypothesis nfimdetndef.d 
|- D = ( N maDet R )
Assertion nfimdetndef 
|- ( N e/ Fin -> D = (/) )

Proof

Step Hyp Ref Expression
1 nfimdetndef.d 
 |-  D = ( N maDet R )
2 eqid 
 |-  ( N Mat R ) = ( N Mat R )
3 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
4 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
5 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
6 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
9 1 2 3 4 5 6 7 8 mdetfval 
 |-  D = ( m e. ( Base ` ( N Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) )
10 df-nel 
 |-  ( N e/ Fin <-> -. N e. Fin )
11 10 biimpi 
 |-  ( N e/ Fin -> -. N e. Fin )
12 11 intnanrd 
 |-  ( N e/ Fin -> -. ( N e. Fin /\ R e. _V ) )
13 matbas0 
 |-  ( -. ( N e. Fin /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) )
14 12 13 syl 
 |-  ( N e/ Fin -> ( Base ` ( N Mat R ) ) = (/) )
15 14 mpteq1d 
 |-  ( N e/ Fin -> ( m e. ( Base ` ( N Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. (/) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
16 mpt0 
 |-  ( m e. (/) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/)
17 15 16 eqtrdi 
 |-  ( N e/ Fin -> ( m e. ( Base ` ( N Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/) )
18 9 17 syl5eq 
 |-  ( N e/ Fin -> D = (/) )