Metamath Proof Explorer


Theorem cnlmodlem2

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

Ref Expression
Hypothesis cnlmod.w W = Base ndx + ndx + Scalar ndx fld ndx ×
Assertion cnlmodlem2 + W = +

Proof

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