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 ⊢ A = N Mat R
marepvcl.b ⊢ B = Base A
marepvcl.v ⊢ V = Base R N
ma1repvcl.1 ⊢ 1 ˙ = 1 A
Assertion ma1repvcl ⊢ R ∈ Ring ∧ N ∈ Fin ∧ C ∈ V ∧ K ∈ N → 1 ˙ N matRepV R C ⁡ K ∈ B

Proof

Step Hyp Ref Expression
1 marepvcl.a ⊢ A = N Mat R
2 marepvcl.b ⊢ B = Base A
3 marepvcl.v ⊢ V = Base R N
4 ma1repvcl.1 ⊢ 1 ˙ = 1 A
5 simpll ⊢ R ∈ Ring ∧ N ∈ Fin ∧ C ∈ V ∧ K ∈ N → R ∈ Ring
6 1 fveq2i ⊢ 1 A = 1 N Mat R
7 4 6 eqtri ⊢ 1 ˙ = 1 N Mat R
8 1 2 7 mat1bas ⊢ R ∈ Ring ∧ N ∈ Fin → 1 ˙ ∈ B
9 8 anim1i ⊢ R ∈ Ring ∧ N ∈ Fin ∧ C ∈ V ∧ K ∈ N → 1 ˙ ∈ B ∧ C ∈ V ∧ K ∈ N
10 3anass ⊢ 1 ˙ ∈ B ∧ C ∈ V ∧ K ∈ N ↔ 1 ˙ ∈ B ∧ C ∈ V ∧ K ∈ N
11 9 10 sylibr ⊢ R ∈ Ring ∧ N ∈ Fin ∧ C ∈ V ∧ K ∈ N → 1 ˙ ∈ B ∧ C ∈ V ∧ K ∈ N
12 1 2 3 marepvcl ⊢ R ∈ Ring ∧ 1 ˙ ∈ B ∧ C ∈ V ∧ K ∈ N → 1 ˙ N matRepV R C ⁡ K ∈ B
13 5 11 12 syl2anc ⊢ R ∈ Ring ∧ N ∈ Fin ∧ C ∈ V ∧ K ∈ N → 1 ˙ N matRepV R C ⁡ K ∈ B