mdetrsca2

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

	Ref	Expression
Hypotheses	mdetrsca2.d	$⊢ D = N maDet R$
	mdetrsca2.k	$⊢ K = {Base}_{R}$
	mdetrsca2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetrsca2.r	$⊢ φ \to R \in CRing$
	mdetrsca2.n	$⊢ φ \to N \in Fin$
	mdetrsca2.x	$⊢ (φ \land i \in N \land j \in N) \to X \in K$
	mdetrsca2.y	$⊢ (φ \land i \in N \land j \in N) \to Y \in K$
	mdetrsca2.f	$⊢ φ \to F \in K$
	mdetrsca2.i	$⊢ φ \to I \in N$
Assertion	mdetrsca2	$⊢ φ \to D ((i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y))) = F \underset{˙}{\cdot} D ((i \in N, j \in N ⟼ if (i = I, X, Y)))$

Proof

Step	Hyp	Ref	Expression
1		mdetrsca2.d	$⊢ D = N maDet R$
2		mdetrsca2.k	$⊢ K = {Base}_{R}$
3		mdetrsca2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		mdetrsca2.r	$⊢ φ \to R \in CRing$
5		mdetrsca2.n	$⊢ φ \to N \in Fin$
6		mdetrsca2.x	$⊢ (φ \land i \in N \land j \in N) \to X \in K$
7		mdetrsca2.y	$⊢ (φ \land i \in N \land j \in N) \to Y \in K$
8		mdetrsca2.f	$⊢ φ \to F \in K$
9		mdetrsca2.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	8	3ad2ant1	$⊢ (φ \land i \in N \land j \in N) \to F \in K$
16	2 3	ringcl	$⊢ (R \in Ring \land F \in K \land X \in K) \to F \underset{˙}{\cdot} X \in K$
17	14 15 6 16	syl3anc	$⊢ (φ \land i \in N \land j \in N) \to F \underset{˙}{\cdot} X \in K$
18	17 7	ifcld	$⊢ (φ \land i \in N \land j \in N) \to if (i = I, F \underset{˙}{\cdot} X, Y) \in K$
19	10 2 11 5 4 18	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) \in {Base}_{(N Mat R)}$
20	6 7	ifcld	$⊢ (φ \land i \in N \land j \in N) \to if (i = I, X, Y) \in K$
21	10 2 11 5 4 20	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ if (i = I, X, Y)) \in {Base}_{(N Mat R)}$
22		snex	$⊢ \{I\} \in V$
23	22	a1i	$⊢ φ \to \{I\} \in V$
24	8	3ad2ant1	$⊢ (φ \land i \in \{I\} \land j \in N) \to F \in K$
25	9	snssd	$⊢ φ \to \{I\} \subseteq N$
26	25	sselda	$⊢ (φ \land i \in \{I\}) \to i \in N$
27	26	3adant3	$⊢ (φ \land i \in \{I\} \land j \in N) \to i \in N$
28	27 6	syld3an2	$⊢ (φ \land i \in \{I\} \land j \in N) \to X \in K$
29		fconstmpo	$⊢ (\{I\} \times N) \times \{F\} = (i \in \{I\}, j \in N ⟼ F)$
30	29	a1i	$⊢ φ \to (\{I\} \times N) \times \{F\} = (i \in \{I\}, j \in N ⟼ F)$
31		eqidd	$⊢ φ \to (i \in \{I\}, j \in N ⟼ X) = (i \in \{I\}, j \in N ⟼ X)$
32	23 5 24 28 30 31	offval22	$⊢ φ \to ((\{I\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} (i \in \{I\}, j \in N ⟼ X) = (i \in \{I\}, j \in N ⟼ F \underset{˙}{\cdot} X)$
33		mposnif	$⊢ (i \in \{I\}, j \in N ⟼ if (i = I, X, Y)) = (i \in \{I\}, j \in N ⟼ X)$
34	33	oveq2i	$⊢ ((\{I\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} (i \in \{I\}, j \in N ⟼ if (i = I, X, Y)) = ((\{I\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} (i \in \{I\}, j \in N ⟼ X)$
35		mposnif	$⊢ (i \in \{I\}, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) = (i \in \{I\}, j \in N ⟼ F \underset{˙}{\cdot} X)$
36	32 34 35	3eqtr4g	$⊢ φ \to ((\{I\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} (i \in \{I\}, j \in N ⟼ if (i = I, X, Y)) = (i \in \{I\}, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y))$
37		ssid	$⊢ N \subseteq N$
38		resmpo	$⊢ (\{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, X, Y)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, X, Y))$
39	25 37 38	sylancl	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, X, Y)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, X, Y))$
40	39	oveq2d	$⊢ φ \to ((\{I\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({(i \in N, j \in N ⟼ if (i = I, X, Y)) ↾}_{(\{I\} \times N)}) = ((\{I\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} (i \in \{I\}, j \in N ⟼ if (i = I, X, Y))$
41		resmpo	$⊢ (\{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y))$
42	25 37 41	sylancl	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) ↾}_{(\{I\} \times N)} = (i \in \{I\}, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y))$
43	36 40 42	3eqtr4rd	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) ↾}_{(\{I\} \times N)} = ((\{I\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({(i \in N, j \in N ⟼ if (i = I, X, Y)) ↾}_{(\{I\} \times N)})$
44		eldifsni	$⊢ i \in (N ∖ \{I\}) \to i \neq I$
45	44	3ad2ant2	$⊢ (φ \land i \in (N ∖ \{I\}) \land j \in N) \to i \neq I$
46	45	neneqd	$⊢ (φ \land i \in (N ∖ \{I\}) \land j \in N) \to \neg i = I$
47		iffalse	$⊢ \neg i = I \to if (i = I, F \underset{˙}{\cdot} X, Y) = Y$
48		iffalse	$⊢ \neg i = I \to if (i = I, X, Y) = Y$
49	47 48	eqtr4d	$⊢ \neg i = I \to if (i = I, F \underset{˙}{\cdot} X, Y) = if (i = I, X, Y)$
50	46 49	syl	$⊢ (φ \land i \in (N ∖ \{I\}) \land j \in N) \to if (i = I, F \underset{˙}{\cdot} X, Y) = if (i = I, X, Y)$
51	50	mpoeq3dva	$⊢ φ \to (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X, Y))$
52		difss	$⊢ N ∖ \{I\} \subseteq N$
53		resmpo	$⊢ (N ∖ \{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y))$
54	52 37 53	mp2an	$⊢ {(i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y))$
55		resmpo	$⊢ (N ∖ \{I\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = I, X, Y)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X, Y))$
56	52 37 55	mp2an	$⊢ {(i \in N, j \in N ⟼ if (i = I, X, Y)) ↾}_{((N ∖ \{I\}) \times N)} = (i \in (N ∖ \{I\}), j \in N ⟼ if (i = I, X, Y))$
57	51 54 56	3eqtr4g	$⊢ φ \to {(i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y)) ↾}_{((N ∖ \{I\}) \times N)} = {(i \in N, j \in N ⟼ if (i = I, X, Y)) ↾}_{((N ∖ \{I\}) \times N)}$
58	1 10 11 2 3 4 19 8 21 9 43 57	mdetrsca	$⊢ φ \to D ((i \in N, j \in N ⟼ if (i = I, F \underset{˙}{\cdot} X, Y))) = F \underset{˙}{\cdot} D ((i \in N, j \in N ⟼ if (i = I, X, Y)))$

Metamath Proof Explorer

Theorem mdetrsca2

Proof