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

Metamath Proof Explorer

Theorem ma1repvcl

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

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

Proof

Step Hyp Ref Expression
1 marepvcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 marepvcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 marepvcl.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4 ma1repvcl.1 ⊢ 1 = ( 1r ‘ 𝐴 )
5 simpll ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
6 1 fveq2i ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
7 4 6 eqtri ⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
8 1 2 7 mat1bas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 1 ∈ 𝐵 )
9 8 anim1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( 1 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) )
10 3anass ⊢ ( ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ↔ ( 1 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) )
11 9 10 sylibr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) )
12 1 2 3 marepvcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) ∈ 𝐵 )
13 5 11 12 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) ∈ 𝐵 )