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=NMatR
marepvcl.b ⊢B=BaseA
marepvcl.v ⊢V=BaseRN
Assertion marepvcl ⊢R∈Ring∧M∈B∧C∈V∧K∈N→MNmatRepVRC⁡K∈B

Proof

Step Hyp Ref Expression
1 marepvcl.a ⊢A=NMatR
2 marepvcl.b ⊢B=BaseA
3 marepvcl.v ⊢V=BaseRN
4 eqid ⊢NmatRepVR=NmatRepVR
5 1 2 4 3 marepvval ⊢M∈B∧C∈V∧K∈N→MNmatRepVRC⁡K=i∈N,j∈N⟼ifj=KC⁡iiMj
6 5 adantl ⊢R∈Ring∧M∈B∧C∈V∧K∈N→MNmatRepVRC⁡K=i∈N,j∈N⟼ifj=KC⁡iiMj
7 eqid ⊢BaseR=BaseR
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∈BaseRN→C:N⟶BaseR
14 ffvelcdm ⊢C:N⟶BaseR∧i∈N→C⁡i∈BaseR
15 14 ex ⊢C:N⟶BaseR→i∈N→C⁡i∈BaseR
16 13 15 syl ⊢C∈BaseRN→i∈N→C⁡i∈BaseR
17 16 3 eleq2s ⊢C∈V→i∈N→C⁡i∈BaseR
18 17 3ad2ant2 ⊢M∈B∧C∈V∧K∈N→i∈N→C⁡i∈BaseR
19 18 adantl ⊢R∈Ring∧M∈B∧C∈V∧K∈N→i∈N→C⁡i∈BaseR
20 19 imp ⊢R∈Ring∧M∈B∧C∈V∧K∈N∧i∈N→C⁡i∈BaseR
21 20 3adant3 ⊢R∈Ring∧M∈B∧C∈V∧K∈N∧i∈N∧j∈N→C⁡i∈BaseR
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∈BaseA
25 24 biimpi ⊢M∈B→M∈BaseA
26 25 3ad2ant1 ⊢M∈B∧C∈V∧K∈N→M∈BaseA
27 26 adantl ⊢R∈Ring∧M∈B∧C∈V∧K∈N→M∈BaseA
28 27 3ad2ant1 ⊢R∈Ring∧M∈B∧C∈V∧K∈N∧i∈N∧j∈N→M∈BaseA
29 1 7 matecl ⊢i∈N∧j∈N∧M∈BaseA→iMj∈BaseR
30 22 23 28 29 syl3anc ⊢R∈Ring∧M∈B∧C∈V∧K∈N∧i∈N∧j∈N→iMj∈BaseR
31 21 30 ifcld ⊢R∈Ring∧M∈B∧C∈V∧K∈N∧i∈N∧j∈N→ifj=KC⁡iiMj∈BaseR
32 1 7 2 11 12 31 matbas2d ⊢R∈Ring∧M∈B∧C∈V∧K∈N→i∈N,j∈N⟼ifj=KC⁡iiMj∈B
33 6 32 eqeltrd ⊢R∈Ring∧M∈B∧C∈V∧K∈N→MNmatRepVRC⁡K∈B