Metamath Proof Explorer

Theorem cpm2mfval

Description: Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019)

Ref Expression
Hypotheses cpm2mfval.i ⊢I=NcPolyMatToMatR
cpm2mfval.s ⊢S=NConstPolyMatR
Assertion cpm2mfval ⊢N∈Fin∧R∈V→I=m∈S⟼x∈N,y∈N⟼coe1⁡xmy⁡0

Proof

Step Hyp Ref Expression
1 cpm2mfval.i ⊢I=NcPolyMatToMatR
2 cpm2mfval.s ⊢S=NConstPolyMatR
3 df-cpmat2mat ⊢cPolyMatToMat=n∈Fin,r∈V⟼m∈nConstPolyMatr⟼x∈n,y∈n⟼coe1⁡xmy⁡0
4 3 a1i ⊢N∈Fin∧R∈V→cPolyMatToMat=n∈Fin,r∈V⟼m∈nConstPolyMatr⟼x∈n,y∈n⟼coe1⁡xmy⁡0
5 oveq12 ⊢n=N∧r=R→nConstPolyMatr=NConstPolyMatR
6 5 2 eqtr4di ⊢n=N∧r=R→nConstPolyMatr=S
7 simpl ⊢n=N∧r=R→n=N
8 eqidd ⊢n=N∧r=R→coe1⁡xmy⁡0=coe1⁡xmy⁡0
9 7 7 8 mpoeq123dv ⊢n=N∧r=R→x∈n,y∈n⟼coe1⁡xmy⁡0=x∈N,y∈N⟼coe1⁡xmy⁡0
10 6 9 mpteq12dv ⊢n=N∧r=R→m∈nConstPolyMatr⟼x∈n,y∈n⟼coe1⁡xmy⁡0=m∈S⟼x∈N,y∈N⟼coe1⁡xmy⁡0
11 10 adantl ⊢N∈Fin∧R∈V∧n=N∧r=R→m∈nConstPolyMatr⟼x∈n,y∈n⟼coe1⁡xmy⁡0=m∈S⟼x∈N,y∈N⟼coe1⁡xmy⁡0
12 simpl ⊢N∈Fin∧R∈V→N∈Fin
13 elex ⊢R∈V→R∈V
14 13 adantl ⊢N∈Fin∧R∈V→R∈V
15 2 ovexi ⊢S∈V
16 mptexg ⊢S∈V→m∈S⟼x∈N,y∈N⟼coe1⁡xmy⁡0∈V
17 15 16 mp1i ⊢N∈Fin∧R∈V→m∈S⟼x∈N,y∈N⟼coe1⁡xmy⁡0∈V
18 4 11 12 14 17 ovmpod ⊢N∈Fin∧R∈V→NcPolyMatToMatR=m∈S⟼x∈N,y∈N⟼coe1⁡xmy⁡0
19 1 18 eqtrid ⊢N∈Fin∧R∈V→I=m∈S⟼x∈N,y∈N⟼coe1⁡xmy⁡0