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 ˙ = 0 R
mdetralt2.r φ R CRing
mdetralt2.n φ N Fin
mdetralt2.x φ j N X K
mdetralt2.y φ i N j N Y K
mdetralt2.i φ I N
mdetralt2.j φ J N
mdetralt2.ij φ I J
Assertion mdetralt2 φ D i N , j 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 ˙ = 0 R
4 mdetralt2.r φ R CRing
5 mdetralt2.n φ N Fin
6 mdetralt2.x φ j N X K
7 mdetralt2.y φ i N j N Y K
8 mdetralt2.i φ I N
9 mdetralt2.j φ J N
10 mdetralt2.ij φ I J
11 eqid N Mat R = N Mat R
12 eqid Base N Mat R = Base N Mat R
13 6 3adant2 φ i N j N X K
14 13 7 ifcld φ i N j N if i = J X Y K
15 13 14 ifcld φ i N j N if i = I X if i = J X Y K
16 11 2 12 5 4 15 matbas2d φ i N , j N if i = I X if i = J X Y Base N Mat R
17 eqidd φ w N i N , j N if i = I X if i = J X Y = i N , j 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 φ w 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 φ w N i = I j = w X = w / j X
22 19 21 eqtrd φ w N i = I j = w if i = I X if i = J X Y = w / j X
23 eqidd φ w N i = I N = N
24 8 adantr φ w N I N
25 simpr φ w N w N
26 nfv j φ w N
27 nfcsb1v _ j w / j X
28 27 nfel1 j w / j X K
29 26 28 nfim j φ w N w / j X K
30 eleq1w j = w j N w N
31 30 anbi2d j = w φ j N φ w N
32 20 eleq1d j = w X K w / j X K
33 31 32 imbi12d j = w φ j N X K φ w N w / j X K
34 29 33 6 chvarfv φ w N w / j X K
35 nfv i φ w N
36 nfcv _ j I
37 nfcv _ i w
38 nfcv _ i w / j X
39 17 22 23 24 25 34 35 26 36 37 38 27 ovmpodxf φ w N I i N , j 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 φ w N i = J j = w if i = I X if i = J X Y = X
45 20 ad2antll φ w N i = J j = w X = w / j X
46 44 45 eqtrd φ w N i = J j = w if i = I X if i = J X Y = w / j X
47 eqidd φ w N i = J N = N
48 9 adantr φ w N J N
49 nfcv _ j J
50 17 46 47 48 25 34 35 26 49 37 38 27 ovmpodxf φ w N J i N , j N if i = I X if i = J X Y w = w / j X
51 39 50 eqtr4d φ w N I i N , j N if i = I X if i = J X Y w = J i N , j N if i = I X if i = J X Y w
52 51 ralrimiva φ w N I i N , j N if i = I X if i = J X Y w = J i N , j N if i = I X if i = J X Y w
53 1 11 12 3 4 16 8 9 10 52 mdetralt φ D i N , j N if i = I X if i = J X Y = 0 ˙