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 𝑅 ) 𝐶 ) ‘ 𝐾 ) ∈ 𝐵 )