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

Metamath Proof Explorer

Theorem marepvcl

Description: Closure of the column replacement function for square matrices. (Contributed by AV, 14-Feb-2019) (Revised by AV, 26-Feb-2019)

Ref Expression
Hypotheses marepvcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
marepvcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
marepvcl.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
Assertion marepvcl ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( ( 𝑀 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 marepvcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 marepvcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 marepvcl.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4 eqid ⊢ ( 𝑁 matRepV 𝑅 ) = ( 𝑁 matRepV 𝑅 )
5 1 2 4 3 marepvval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑀 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
6 5 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( ( 𝑀 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
9 8 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
10 9 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
11 10 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
12 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
13 elmapi ⊢ ( 𝐶 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) → 𝐶 : 𝑁 ⟶ ( Base ‘ 𝑅 ) )
14 ffvelcdm ⊢ ( ( 𝐶 : 𝑁 ⟶ ( Base ‘ 𝑅 ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) )
15 14 ex ⊢ ( 𝐶 : 𝑁 ⟶ ( Base ‘ 𝑅 ) → ( 𝑖 ∈ 𝑁 → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
16 13 15 syl ⊢ ( 𝐶 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) → ( 𝑖 ∈ 𝑁 → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
17 16 3 eleq2s ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑖 ∈ 𝑁 → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
18 17 3ad2ant2 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
19 18 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
20 19 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) )
21 20 3adant3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝐶 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) )
22 simp2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
23 simp3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
24 2 eleq2i ⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
25 24 biimpi ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
26 25 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
27 26 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
28 27 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
29 1 7 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
30 22 23 28 29 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
31 21 30 ifcld ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
32 1 7 2 11 12 31 matbas2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 )
33 6 32 eqeltrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( ( 𝑀 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) ∈ 𝐵 )