submatminr1

Description: If we take a submatrix by removing the row I and column J , then the result is the same on the matrix with row I and column J modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020)

	Ref	Expression
Hypotheses	submateq.a	$⊢ A = (1 \dots N) Mat R$
	submateq.b	$⊢ B = {Base}_{A}$
	submateq.n	$⊢ φ \to N \in ℕ$
	submateq.i	$⊢ φ \to I \in (1 \dots N)$
	submateq.j	$⊢ φ \to J \in (1 \dots N)$
	submatminr1.r	$⊢ φ \to R \in Ring$
	submatminr1.m	$⊢ φ \to M \in B$
	submatminr1.e	$⊢ E = I ((1 \dots N) minMatR1 R) (M) J$
Assertion	submatminr1	$⊢ φ \to I {subMat}_{1} (M) J = I {subMat}_{1} (E) J$

Proof

Step	Hyp	Ref	Expression
1		submateq.a	$⊢ A = (1 \dots N) Mat R$
2		submateq.b	$⊢ B = {Base}_{A}$
3		submateq.n	$⊢ φ \to N \in ℕ$
4		submateq.i	$⊢ φ \to I \in (1 \dots N)$
5		submateq.j	$⊢ φ \to J \in (1 \dots N)$
6		submatminr1.r	$⊢ φ \to R \in Ring$
7		submatminr1.m	$⊢ φ \to M \in B$
8		submatminr1.e	$⊢ E = I ((1 \dots N) minMatR1 R) (M) J$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	1 2 9	minmar1marrep	$⊢ (R \in Ring \land M \in B) \to ((1 \dots N) minMatR1 R) (M) = M ((1 \dots N) matRRep R) 1_{R}$
11	6 7 10	syl2anc	$⊢ φ \to ((1 \dots N) minMatR1 R) (M) = M ((1 \dots N) matRRep R) 1_{R}$
12	11	oveqd	$⊢ φ \to I ((1 \dots N) minMatR1 R) (M) J = I (M ((1 \dots N) matRRep R) 1_{R}) J$
13	8 12	syl5eq	$⊢ φ \to E = I (M ((1 \dots N) matRRep R) 1_{R}) J$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	14 9	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
16	6 15	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
17	1 2	marrepcl	$⊢ ((R \in Ring \land M \in B \land 1_{R} \in {Base}_{R}) \land (I \in (1 \dots N) \land J \in (1 \dots N))) \to I (M ((1 \dots N) matRRep R) 1_{R}) J \in B$
18	6 7 16 4 5 17	syl32anc	$⊢ φ \to I (M ((1 \dots N) matRRep R) 1_{R}) J \in B$
19	13 18	eqeltrd	$⊢ φ \to E \in B$
20	13	3ad2ant1	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to E = I (M ((1 \dots N) matRRep R) 1_{R}) J$
21	20	oveqd	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i E j = i (I (M ((1 \dots N) matRRep R) 1_{R}) J) j$
22	7	3ad2ant1	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to M \in B$
23	16	3ad2ant1	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to 1_{R} \in {Base}_{R}$
24	4	3ad2ant1	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to I \in (1 \dots N)$
25	5	3ad2ant1	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to J \in (1 \dots N)$
26		simp2	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i \in ((1 \dots N) ∖ \{I\})$
27	26	eldifad	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i \in (1 \dots N)$
28		simp3	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to j \in ((1 \dots N) ∖ \{J\})$
29	28	eldifad	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to j \in (1 \dots N)$
30		eqid	$⊢ (1 \dots N) matRRep R = (1 \dots N) matRRep R$
31		eqid	$⊢ 0_{R} = 0_{R}$
32	1 2 30 31	marrepeval	$⊢ ((M \in B \land 1_{R} \in {Base}_{R}) \land (I \in (1 \dots N) \land J \in (1 \dots N)) \land (i \in (1 \dots N) \land j \in (1 \dots N))) \to i (I (M ((1 \dots N) matRRep R) 1_{R}) J) j = if (i = I, if (j = J, 1_{R}, 0_{R}), i M j)$
33	22 23 24 25 27 29 32	syl222anc	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i (I (M ((1 \dots N) matRRep R) 1_{R}) J) j = if (i = I, if (j = J, 1_{R}, 0_{R}), i M j)$
34		eldifsn	$⊢ i \in ((1 \dots N) ∖ \{I\}) \leftrightarrow (i \in (1 \dots N) \land i \neq I)$
35	26 34	sylib	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to (i \in (1 \dots N) \land i \neq I)$
36	35	simprd	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i \neq I$
37	36	neneqd	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to \neg i = I$
38	37	iffalsed	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to if (i = I, if (j = J, 1_{R}, 0_{R}), i M j) = i M j$
39	21 33 38	3eqtrrd	$⊢ (φ \land i \in ((1 \dots N) ∖ \{I\}) \land j \in ((1 \dots N) ∖ \{J\})) \to i M j = i E j$
40	1 2 3 4 5 7 19 39	submateq	$⊢ φ \to I {subMat}_{1} (M) J = I {subMat}_{1} (E) J$

Metamath Proof Explorer

Theorem submatminr1

Proof