Theorem 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	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
	submateq.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	submateq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	submateq.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
	submateq.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
	submatminr1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	submatminr1.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
	submatminr1.e	⊢ 𝐸 = ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 )
Assertion	submatminr1	⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) = ( 𝐼 ( subMat1 ‘ 𝐸 ) 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		submateq.a	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
2		submateq.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		submateq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		submateq.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
5		submateq.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
6		submatminr1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		submatminr1.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
8		submatminr1.e	⊢ 𝐸 = ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 )
9		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10	1 2 9	minmar1marrep	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
11	6 7 10	syl2anc	⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
12	11	oveqd	⊢ ( 𝜑 → ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) = ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) )
13	8 12	syl5eq	⊢ ( 𝜑 → 𝐸 = ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) )
14		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15	14 9	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
16	6 15	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
17	1 2	marrepcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) ∈ 𝐵 )
18	6 7 16 4 5 17	syl32anc	⊢ ( 𝜑 → ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) ∈ 𝐵 )
19	13 18	eqeltrd	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
20	13	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝐸 = ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) )
21	20	oveqd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝑖 𝐸 𝑗 ) = ( 𝑖 ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) 𝑗 ) )
22	7	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝑀 ∈ 𝐵 )
23	16	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
24	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
25	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝐽 ∈ ( 1 ... 𝑁 ) )
26		simp2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) )
27	26	eldifad	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
28		simp3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) )
29	28	eldifad	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
30		eqid	⊢ ( ( 1 ... 𝑁 ) matRRep 𝑅 ) = ( ( 1 ... 𝑁 ) matRRep 𝑅 )
31		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
32	1 2 30 31	marrepeval	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝑖 ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) 𝑗 ) = if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) )
33	22 23 24 25 27 29 32	syl222anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝑖 ( 𝐼 ( 𝑀 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐽 ) 𝑗 ) = if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) )
34		eldifsn	⊢ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ↔ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑖 ≠ 𝐼 ) )
35	26 34	sylib	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑖 ≠ 𝐼 ) )
36	35	simprd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → 𝑖 ≠ 𝐼 )
37	36	neneqd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → ¬ 𝑖 = 𝐼 )
38	37	iffalsed	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) = ( 𝑖 𝑀 𝑗 ) )
39	21 33 38	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑖 𝐸 𝑗 ) )
40	1 2 3 4 5 7 19 39	submateq	⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) = ( 𝐼 ( subMat1 ‘ 𝐸 ) 𝐽 ) )