Metamath Proof Explorer


Theorem cnlmodlem2

Description: Lemma 2 for cnlmod . (Contributed by AV, 20-Sep-2021)

Ref Expression
Hypothesis cnlmod.w W=Basendx+ndx+Scalarndxfldndx×
Assertion cnlmodlem2 +W=+

Proof

Step Hyp Ref Expression
1 cnlmod.w W=Basendx+ndx+Scalarndxfldndx×
2 addex +V
3 qdass Basendx+ndx+Scalarndxfldndx×=Basendx+ndx+Scalarndxfldndx×
4 1 3 eqtri W=Basendx+ndx+Scalarndxfldndx×
5 4 lmodplusg +V+=+W
6 5 eqcomd +V+W=+
7 2 6 ax-mp +W=+