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