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

Metamath Proof Explorer

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 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )