Theorem submaval

Description: Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018)

	Ref	Expression
Hypotheses	submafval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	submafval.q	⊢ 𝑄 = ( 𝑁 subMat 𝑅 )
	submafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	submaval	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )

Proof

Step	Hyp	Ref	Expression
1		submafval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		submafval.q	⊢ 𝑄 = ( 𝑁 subMat 𝑅 )
3		submafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4	1 2 3	submaval0	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑄 ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ ( 𝑁 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) )
5	4	3ad2ant1	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ ( 𝑁 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) )
6		simp2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → 𝐾 ∈ 𝑁 )
7		simpl3	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑘 = 𝐾 ) → 𝐿 ∈ 𝑁 )
8	1 3	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
9	8	simpld	⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
10		diffi	⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝑘 } ) ∈ Fin )
11	9 10	syl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∖ { 𝑘 } ) ∈ Fin )
12		diffi	⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝑙 } ) ∈ Fin )
13	9 12	syl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∖ { 𝑙 } ) ∈ Fin )
14	11 13	jca	⊢ ( 𝑀 ∈ 𝐵 → ( ( 𝑁 ∖ { 𝑘 } ) ∈ Fin ∧ ( 𝑁 ∖ { 𝑙 } ) ∈ Fin ) )
15	14	3ad2ant1	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝑁 ∖ { 𝑘 } ) ∈ Fin ∧ ( 𝑁 ∖ { 𝑙 } ) ∈ Fin ) )
16	15	adantr	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → ( ( 𝑁 ∖ { 𝑘 } ) ∈ Fin ∧ ( 𝑁 ∖ { 𝑙 } ) ∈ Fin ) )
17		mpoexga	⊢ ( ( ( 𝑁 ∖ { 𝑘 } ) ∈ Fin ∧ ( 𝑁 ∖ { 𝑙 } ) ∈ Fin ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ V )
18	16 17	syl	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ V )
19		sneq	⊢ ( 𝑘 = 𝐾 → { 𝑘 } = { 𝐾 } )
20	19	difeq2d	⊢ ( 𝑘 = 𝐾 → ( 𝑁 ∖ { 𝑘 } ) = ( 𝑁 ∖ { 𝐾 } ) )
21	20	adantr	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) → ( 𝑁 ∖ { 𝑘 } ) = ( 𝑁 ∖ { 𝐾 } ) )
22		sneq	⊢ ( 𝑙 = 𝐿 → { 𝑙 } = { 𝐿 } )
23	22	difeq2d	⊢ ( 𝑙 = 𝐿 → ( 𝑁 ∖ { 𝑙 } ) = ( 𝑁 ∖ { 𝐿 } ) )
24	23	adantl	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) → ( 𝑁 ∖ { 𝑙 } ) = ( 𝑁 ∖ { 𝐿 } ) )
25		eqidd	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
26	21 24 25	mpoeq123dv	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
27	26	adantl	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
28	6 7 18 27	ovmpodv2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝑄 ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ ( 𝑁 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) )
29	5 28	mpd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )