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 ⊢ A = N Mat R
marepvcl.b ⊢ B = Base A
marepvcl.v ⊢ V = Base R N
Assertion marepvcl ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → M 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 eqid ⊢ N matRepV R = N matRepV R
5 1 2 4 3 marepvval ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N → M N matRepV R C ⁡ K = i ∈ N , j ∈ N ⟼ if j = K C ⁡ i i M j
6 5 adantl ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → M N matRepV R C ⁡ K = i ∈ N , j ∈ N ⟼ if j = K C ⁡ i i M j
7 eqid ⊢ Base R = Base R
8 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
9 8 simpld ⊢ M ∈ B → N ∈ Fin
10 9 3ad2ant1 ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N → N ∈ Fin
11 10 adantl ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → N ∈ Fin
12 simpl ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → R ∈ Ring
13 elmapi ⊢ C ∈ Base R N → C : N ⟶ Base R
14 ffvelcdm ⊢ C : N ⟶ Base R ∧ i ∈ N → C ⁡ i ∈ Base R
15 14 ex ⊢ C : N ⟶ Base R → i ∈ N → C ⁡ i ∈ Base R
16 13 15 syl ⊢ C ∈ Base R N → i ∈ N → C ⁡ i ∈ Base R
17 16 3 eleq2s ⊢ C ∈ V → i ∈ N → C ⁡ i ∈ Base R
18 17 3ad2ant2 ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N → i ∈ N → C ⁡ i ∈ Base R
19 18 adantl ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → i ∈ N → C ⁡ i ∈ Base R
20 19 imp ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ i ∈ N → C ⁡ i ∈ Base R
21 20 3adant3 ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → C ⁡ i ∈ Base R
22 simp2 ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → i ∈ N
23 simp3 ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → j ∈ N
24 2 eleq2i ⊢ M ∈ B ↔ M ∈ Base A
25 24 biimpi ⊢ M ∈ B → M ∈ Base A
26 25 3ad2ant1 ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N → M ∈ Base A
27 26 adantl ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → M ∈ Base A
28 27 3ad2ant1 ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → M ∈ Base A
29 1 7 matecl ⊢ i ∈ N ∧ j ∈ N ∧ M ∈ Base A → i M j ∈ Base R
30 22 23 28 29 syl3anc ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → i M j ∈ Base R
31 21 30 ifcld ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → if j = K C ⁡ i i M j ∈ Base R
32 1 7 2 11 12 31 matbas2d ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → i ∈ N , j ∈ N ⟼ if j = K C ⁡ i i M j ∈ B
33 6 32 eqeltrd ⊢ R ∈ Ring ∧ M ∈ B ∧ C ∈ V ∧ K ∈ N → M N matRepV R C ⁡ K ∈ B