This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem submaeval

Description: An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018)

		Ref	Expression
	Hypotheses	submafval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
		submafval.q	⊢ 𝑄 = ( 𝑁 subMat 𝑅 )
		submafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	Assertion	submaeval	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) → ( 𝐼 ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) 𝐽 ) = ( 𝐼 𝑀 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		submafval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		submafval.q	⊢ 𝑄 = ( 𝑁 subMat 𝑅 )
3		submafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4	1 2 3	submaval	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
5	4	3expb	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
6	5	3adant3	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
7		simp3l	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) → 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) )
8		simpl3r	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) ∧ 𝑖 = 𝐼 ) → 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) )
9		ovexd	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ V )
10		oveq12	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝐼 𝑀 𝐽 ) )
11	10	adantl	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → ( 𝑖 𝑀 𝑗 ) = ( 𝐼 𝑀 𝐽 ) )
12	7 8 9 11	ovmpodv2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) → ( ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) → ( 𝐼 ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) 𝐽 ) = ( 𝐼 𝑀 𝐽 ) ) )
13	6 12	mpd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝐽 ∈ ( 𝑁 ∖ { 𝐿 } ) ) ) → ( 𝐼 ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) 𝐽 ) = ( 𝐼 𝑀 𝐽 ) )