Metamath Proof Explorer

Theorem cpm2mfval

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

Ref Expression
Hypotheses cpm2mfval.i ⊢ I = N cPolyMatToMat R
cpm2mfval.s ⊢ S = N ConstPolyMat R
Assertion cpm2mfval ⊢ N ∈ Fin ∧ R ∈ V → I = m ∈ S ⟼ x ∈ N , y ∈ N ⟼ coe 1 ⁡ x m y ⁡ 0

Proof

Step Hyp Ref Expression
1 cpm2mfval.i ⊢ I = N cPolyMatToMat R
2 cpm2mfval.s ⊢ S = N ConstPolyMat R
3 df-cpmat2mat ⊢ cPolyMatToMat = n ∈ Fin , r ∈ V ⟼ m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0
4 3 a1i ⊢ N ∈ Fin ∧ R ∈ V → cPolyMatToMat = n ∈ Fin , r ∈ V ⟼ m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0
5 oveq12 ⊢ n = N ∧ r = R → n ConstPolyMat r = N ConstPolyMat R
6 5 2 eqtr4di ⊢ n = N ∧ r = R → n ConstPolyMat r = S
7 simpl ⊢ n = N ∧ r = R → n = N
8 eqidd ⊢ n = N ∧ r = R → coe 1 ⁡ x m y ⁡ 0 = coe 1 ⁡ x m y ⁡ 0
9 7 7 8 mpoeq123dv ⊢ n = N ∧ r = R → x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0 = x ∈ N , y ∈ N ⟼ coe 1 ⁡ x m y ⁡ 0
10 6 9 mpteq12dv ⊢ n = N ∧ r = R → m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0 = m ∈ S ⟼ x ∈ N , y ∈ N ⟼ coe 1 ⁡ x m y ⁡ 0
11 10 adantl ⊢ N ∈ Fin ∧ R ∈ V ∧ n = N ∧ r = R → m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0 = m ∈ S ⟼ x ∈ N , y ∈ N ⟼ coe 1 ⁡ x m y ⁡ 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 ⟼ coe 1 ⁡ x m y ⁡ 0 ∈ V
17 15 16 mp1i ⊢ N ∈ Fin ∧ R ∈ V → m ∈ S ⟼ x ∈ N , y ∈ N ⟼ coe 1 ⁡ x m y ⁡ 0 ∈ V
18 4 11 12 14 17 ovmpod ⊢ N ∈ Fin ∧ R ∈ V → N cPolyMatToMat R = m ∈ S ⟼ x ∈ N , y ∈ N ⟼ coe 1 ⁡ x m y ⁡ 0
19 1 18 syl5eq ⊢ N ∈ Fin ∧ R ∈ V → I = m ∈ S ⟼ x ∈ N , y ∈ N ⟼ coe 1 ⁡ x m y ⁡ 0