mdetrlin2

Description: The determinant function is additive for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018)

	Ref	Expression
Hypotheses	mdetrlin2.d	$⊢ D = N maDet R$
	mdetrlin2.k	$⊢ K = {Base}_{R}$
	mdetrlin2.p	$⊢ \underset{˙}{+} = +_{R}$
	mdetrlin2.r	$⊢ φ \to R \in CRing$
	mdetrlin2.n	$⊢ φ \to N \in Fin$
	mdetrlin2.x	$⊢ (φ \land i \in N \land j \in N) \to X \in K$
	mdetrlin2.y	$⊢ (φ \land i \in N \land j \in N) \to Y \in K$
	mdetrlin2.z	$⊢ (φ \land i \in N \land j \in N) \to Z \in K$
	mdetrlin2.i	$⊢ φ \to I \in N$
Assertion	mdetrlin2	$⊢ φ \to D ((i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z))) = D ((i \in N, j \in N ⟼ if (i = I, X, Z))) \underset{˙}{+} D ((i \in N, j \in N ⟼ if (i = I, Y, Z)))$

Proof

Step	Hyp	Ref	Expression
1		mdetrlin2.d	$⊢ D = N maDet R$
2		mdetrlin2.k	$⊢ K = {Base}_{R}$
3		mdetrlin2.p	$⊢ \underset{˙}{+} = +_{R}$
4		mdetrlin2.r	$⊢ φ \to R \in CRing$
5		mdetrlin2.n	$⊢ φ \to N \in Fin$
6		mdetrlin2.x	$⊢ (φ \land i \in N \land j \in N) \to X \in K$
7		mdetrlin2.y	$⊢ (φ \land i \in N \land j \in N) \to Y \in K$
8		mdetrlin2.z	$⊢ (φ \land i \in N \land j \in N) \to Z \in K$
9		mdetrlin2.i	$⊢ φ \to I \in N$
10		eqid	$⊢ N Mat R = N Mat R$
11		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
12		crngring	$⊢ R \in CRing \to R \in Ring$
13	4 12	syl	$⊢ φ \to R \in Ring$
14	13	3ad2ant1	$⊢ (φ \land i \in N \land j \in N) \to R \in Ring$
15	2 3	ringacl	$⊢ (R \in Ring \land X \in K \land Y \in K) \to X \underset{˙}{+} Y \in K$
16	14 6 7 15	syl3anc	$⊢ (φ \land i \in N \land j \in N) \to X \underset{˙}{+} Y \in K$
17	16 8	ifcld	$⊢ (φ \land i \in N \land j \in N) \to if (i = I, X \underset{˙}{+} Y, Z) \in K$
18	10 2 11 5 4 17	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) \in {Base}_{(N Mat R)}$
19	6 8	ifcld	$⊢ (φ \land i \in N \land j \in N) \to if (i = I, X, Z) \in K$
20	10 2 11 5 4 19	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ if (i = I, X, Z)) \in {Base}_{(N Mat R)}$
21	7 8	ifcld	$⊢ (φ \land i \in N \land j \in N) \to if (i = I, Y, Z) \in K$
22	10 2 11 5 4 21	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ if (i = I, Y, Z)) \in {Base}_{(N Mat R)}$
23		snex	$⊢ \{I\} \in V$
24	23	a1i	$⊢ φ \to \{I\} \in V$
25	9	snssd	$⊢ φ \to \{I\} \subseteq N$
26	25	3ad2ant1	$⊢ (φ \land i \in \{I\} \land j \in N) \to \{I\} \subseteq N$
27		simp2	$⊢ (φ \land i \in \{I\} \land j \in N) \to i \in \{I\}$
28	26 27	sseldd	$⊢ (φ \land i \in \{I\} \land j \in N) \to i \in N$
29	28 6	syld3an2	$⊢ (φ \land i \in \{I\} \land j \in N) \to X \in K$
30	28 7	syld3an2	$⊢ (φ \land i \in \{I\} \land j \in N) \to Y \in K$
31		eqidd	$⊢ φ \to (i \in \{I\}, j \in N ⟼ X) = (i \in \{I\}, j \in N ⟼ X)$
32		eqidd	$⊢ φ \to (i \in \{I\}, j \in N ⟼ Y) = (i \in \{I\}, j \in N ⟼ Y)$
33	24 5 29 30 31 32	offval22	$⊢ φ \to (i \in \{I\}, j \in N ⟼ X) {\underset{˙}{+}}_{f} (i \in \{I\}, j \in N ⟼ Y) = (i \in \{I\}, j \in N ⟼ X \underset{˙}{+} Y)$
34	33	eqcomd	$⊢ φ \to (i \in \{I\}, j \in N ⟼ X \underset{˙}{+} Y) = (i \in \{I\}, j \in N ⟼ X) {\underset{˙}{+}}_{f} (i \in \{I\}, j \in N ⟼ Y)$
35		mposnif	$⊢ (i \in \{I\}, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) = (i \in \{I\}, j \in N ⟼ X \underset{˙}{+} Y)$
36		mposnif	$⊢ (i \in \{I\}, j \in N ⟼ if (i = I, X, Z)) = (i \in \{I\}, j \in N ⟼ X)$
37		mposnif	$⊢ (i \in \{I\}, j \in N ⟼ if (i = I, Y, Z)) = (i \in \{I\}, j \in N ⟼ Y)$
38	36 37	oveq12i	$⊢ (i \in \{I\}, j \in N ⟼ if (i = I, X, Z)) {\underset{˙}{+}}_{f} (i \in \{I\}, j \in N ⟼ if (i = I, Y, Z)) = (i \in \{I\}, j \in N ⟼ X) {\underset{˙}{+}}_{f} (i \in \{I\}, j \in N ⟼ Y)$
39	34 35 38	3eqtr4g	$⊢ φ \to (i \in \{I\}, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) = (i \in \{I\}, j \in N ⟼ if (i = I, X, Z)) {\underset{˙}{+}}_{f} (i \in \{I\}, j \in N ⟼ if (i = I, Y, Z))$
40		ssid	$⊢ N \subseteq N$
41		resmpo	$⊢ (\{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z))$
42	25 40 41	sylancl	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z))$
43		resmpo	$⊢ (\{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, X, Z)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, X, Z))$
44	25 40 43	sylancl	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, X, Z)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, X, Z))$
45		resmpo	$⊢ (\{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, Y, Z)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, Y, Z))$
46	25 40 45	sylancl	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, Y, Z)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, Y, Z))$
47	44 46	oveq12d	$⊢ φ \to ({(i \in N, j \in N ⟼ if (i = I, X, Z)) ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({(i \in N, j \in N ⟼ if (i = I, Y, Z)) ↾}_{(\{I\} \times N)}) = (i \in \{I\}, j \in N ⟼ if (i = I, X, Z)) {\underset{˙}{+}}_{f} (i \in \{I\}, j \in N ⟼ if (i = I, Y, Z))$
48	39 42 47	3eqtr4d	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) ↾}_{(\{I\} \times N)} = ({(i \in N, j \in N ⟼ if (i = I, X, Z)) ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({(i \in N, j \in N ⟼ if (i = I, Y, Z)) ↾}_{(\{I\} \times N)})$
49		eldifsni	$⊢ i \in (N ∖ \{I\}) \to i \neq I$
50	49	neneqd	$⊢ i \in (N ∖ \{I\}) \to \neg i = I$
51		iffalse	$⊢ \neg i = I \to if (i = I, X \underset{˙}{+} Y, Z) = Z$
52		iffalse	$⊢ \neg i = I \to if (i = I, X, Z) = Z$
53	51 52	eqtr4d	$⊢ \neg i = I \to if (i = I, X \underset{˙}{+} Y, Z) = if (i = I, X, Z)$
54	50 53	syl	$⊢ i \in (N ∖ \{I\}) \to if (i = I, X \underset{˙}{+} Y, Z) = if (i = I, X, Z)$
55	54	3ad2ant2	$⊢ (φ \land i \in (N ∖ \{I\}) \land j \in N) \to if (i = I, X \underset{˙}{+} Y, Z) = if (i = I, X, Z)$
56	55	mpoeq3dva	$⊢ φ \to (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X, Z))$
57		difss	$⊢ N ∖ \{I\} \subseteq N$
58		resmpo	$⊢ (N ∖ \{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z))$
59	57 40 58	mp2an	$⊢ {(i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z))$
60		resmpo	$⊢ (N ∖ \{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, X, Z)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X, Z))$
61	57 40 60	mp2an	$⊢ {(i \in N, j \in N ⟼ if (i = I, X, Z)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X, Z))$
62	56 59 61	3eqtr4g	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) ↾}_{((N ∖ \{I\}) \times N)} = {(i \in N, j \in N ⟼ if (i = I, X, Z)) ↾}_{((N ∖ \{I\}) \times N)}$
63		iffalse	$⊢ \neg i = I \to if (i = I, Y, Z) = Z$
64	51 63	eqtr4d	$⊢ \neg i = I \to if (i = I, X \underset{˙}{+} Y, Z) = if (i = I, Y, Z)$
65	50 64	syl	$⊢ i \in (N ∖ \{I\}) \to if (i = I, X \underset{˙}{+} Y, Z) = if (i = I, Y, Z)$
66	65	3ad2ant2	$⊢ (φ \land i \in (N ∖ \{I\}) \land j \in N) \to if (i = I, X \underset{˙}{+} Y, Z) = if (i = I, Y, Z)$
67	66	mpoeq3dva	$⊢ φ \to (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, Y, Z))$
68		resmpo	$⊢ (N ∖ \{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, Y, Z)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, Y, Z))$
69	57 40 68	mp2an	$⊢ {(i \in N, j \in N ⟼ if (i = I, Y, Z)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, Y, Z))$
70	67 59 69	3eqtr4g	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z)) ↾}_{((N ∖ \{I\}) \times N)} = {(i \in N, j \in N ⟼ if (i = I, Y, Z)) ↾}_{((N ∖ \{I\}) \times N)}$
71	1 10 11 3 4 18 20 22 9 48 62 70	mdetrlin	$⊢ φ \to D ((i \in N, j \in N ⟼ if (i = I, X \underset{˙}{+} Y, Z))) = D ((i \in N, j \in N ⟼ if (i = I, X, Z))) \underset{˙}{+} D ((i \in N, j \in N ⟼ if (i = I, Y, Z)))$

Metamath Proof Explorer

Theorem mdetrlin2

Proof