Metamath Proof Explorer

Theorem mdetralt2

Description: The determinant function is alternating regarding rows (matrix is given explicitly by its entries). (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses mdetralt2.d 
|- D = ( N maDet R )
mdetralt2.k 
|- K = ( Base ` R )
mdetralt2.z 
|- .0. = ( 0g ` R )
mdetralt2.r 
|- ( ph -> R e. CRing )
mdetralt2.n 
|- ( ph -> N e. Fin )
mdetralt2.x 
|- ( ( ph /\ j e. N ) -> X e. K )
mdetralt2.y 
|- ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
mdetralt2.i 
|- ( ph -> I e. N )
mdetralt2.j 
|- ( ph -> J e. N )
mdetralt2.ij 
|- ( ph -> I =/= J )
Assertion mdetralt2 
|- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) ) = .0. )

Proof

Step Hyp Ref Expression
1 mdetralt2.d 
 |-  D = ( N maDet R )
2 mdetralt2.k 
 |-  K = ( Base ` R )
3 mdetralt2.z 
 |-  .0. = ( 0g ` R )
4 mdetralt2.r 
 |-  ( ph -> R e. CRing )
5 mdetralt2.n 
 |-  ( ph -> N e. Fin )
6 mdetralt2.x 
 |-  ( ( ph /\ j e. N ) -> X e. K )
7 mdetralt2.y 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
8 mdetralt2.i 
 |-  ( ph -> I e. N )
9 mdetralt2.j 
 |-  ( ph -> J e. N )
10 mdetralt2.ij 
 |-  ( ph -> I =/= J )
11 eqid 
 |-  ( N Mat R ) = ( N Mat R )
12 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
13 6 3adant2 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
14 13 7 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = J , X , Y ) e. K )
15 13 14 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , X , if ( i = J , X , Y ) ) e. K )
16 11 2 12 5 4 15 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) e. ( Base ` ( N Mat R ) ) )
17 eqidd 
 |-  ( ( ph /\ w e. N ) -> ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) = ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) )
18 iftrue 
 |-  ( i = I -> if ( i = I , X , if ( i = J , X , Y ) ) = X )
19 18 ad2antrl 
 |-  ( ( ( ph /\ w e. N ) /\ ( i = I /\ j = w ) ) -> if ( i = I , X , if ( i = J , X , Y ) ) = X )
20 csbeq1a 
 |-  ( j = w -> X = [_ w / j ]_ X )
21 20 ad2antll 
 |-  ( ( ( ph /\ w e. N ) /\ ( i = I /\ j = w ) ) -> X = [_ w / j ]_ X )
22 19 21 eqtrd 
 |-  ( ( ( ph /\ w e. N ) /\ ( i = I /\ j = w ) ) -> if ( i = I , X , if ( i = J , X , Y ) ) = [_ w / j ]_ X )
23 eqidd 
 |-  ( ( ( ph /\ w e. N ) /\ i = I ) -> N = N )
24 8 adantr 
 |-  ( ( ph /\ w e. N ) -> I e. N )
25 simpr 
 |-  ( ( ph /\ w e. N ) -> w e. N )
26 nfv 
 |-  F/ j ( ph /\ w e. N )
27 nfcsb1v 
 |-  F/_ j [_ w / j ]_ X
28 27 nfel1 
 |-  F/ j [_ w / j ]_ X e. K
29 26 28 nfim 
 |-  F/ j ( ( ph /\ w e. N ) -> [_ w / j ]_ X e. K )
30 eleq1w 
 |-  ( j = w -> ( j e. N <-> w e. N ) )
31 30 anbi2d 
 |-  ( j = w -> ( ( ph /\ j e. N ) <-> ( ph /\ w e. N ) ) )
32 20 eleq1d 
 |-  ( j = w -> ( X e. K <-> [_ w / j ]_ X e. K ) )
33 31 32 imbi12d 
 |-  ( j = w -> ( ( ( ph /\ j e. N ) -> X e. K ) <-> ( ( ph /\ w e. N ) -> [_ w / j ]_ X e. K ) ) )
34 29 33 6 chvarfv 
 |-  ( ( ph /\ w e. N ) -> [_ w / j ]_ X e. K )
35 nfv 
 |-  F/ i ( ph /\ w e. N )
36 nfcv 
 |-  F/_ j I
37 nfcv 
 |-  F/_ i w
38 nfcv 
 |-  F/_ i [_ w / j ]_ X
39 17 22 23 24 25 34 35 26 36 37 38 27 ovmpodxf 
 |-  ( ( ph /\ w e. N ) -> ( I ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) w ) = [_ w / j ]_ X )
40 iftrue 
 |-  ( i = J -> if ( i = J , X , Y ) = X )
41 40 ifeq2d 
 |-  ( i = J -> if ( i = I , X , if ( i = J , X , Y ) ) = if ( i = I , X , X ) )
42 ifid 
 |-  if ( i = I , X , X ) = X
43 41 42 eqtrdi 
 |-  ( i = J -> if ( i = I , X , if ( i = J , X , Y ) ) = X )
44 43 ad2antrl 
 |-  ( ( ( ph /\ w e. N ) /\ ( i = J /\ j = w ) ) -> if ( i = I , X , if ( i = J , X , Y ) ) = X )
45 20 ad2antll 
 |-  ( ( ( ph /\ w e. N ) /\ ( i = J /\ j = w ) ) -> X = [_ w / j ]_ X )
46 44 45 eqtrd 
 |-  ( ( ( ph /\ w e. N ) /\ ( i = J /\ j = w ) ) -> if ( i = I , X , if ( i = J , X , Y ) ) = [_ w / j ]_ X )
47 eqidd 
 |-  ( ( ( ph /\ w e. N ) /\ i = J ) -> N = N )
48 9 adantr 
 |-  ( ( ph /\ w e. N ) -> J e. N )
49 nfcv 
 |-  F/_ j J
50 17 46 47 48 25 34 35 26 49 37 38 27 ovmpodxf 
 |-  ( ( ph /\ w e. N ) -> ( J ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) w ) = [_ w / j ]_ X )
51 39 50 eqtr4d 
 |-  ( ( ph /\ w e. N ) -> ( I ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) w ) = ( J ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) w ) )
52 51 ralrimiva 
 |-  ( ph -> A. w e. N ( I ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) w ) = ( J ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) w ) )
53 1 11 12 3 4 16 8 9 10 52 mdetralt 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) ) = .0. )