Metamath Proof Explorer


Theorem zlmlem

Description: Lemma for zlmbas and zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)

Ref Expression
Hypotheses zlmbas.w W=ℤModG
zlmlem.2 E=SlotEndx
zlmlem.3 EndxScalarndx
zlmlem.4 Endxndx
Assertion zlmlem EG=EW

Proof

Step Hyp Ref Expression
1 zlmbas.w W=ℤModG
2 zlmlem.2 E=SlotEndx
3 zlmlem.3 EndxScalarndx
4 zlmlem.4 Endxndx
5 2 3 setsnid EG=EGsSetScalarndxring
6 2 4 setsnid EGsSetScalarndxring=EGsSetScalarndxringsSetndxG
7 5 6 eqtri EG=EGsSetScalarndxringsSetndxG
8 eqid G=G
9 1 8 zlmval GVW=GsSetScalarndxringsSetndxG
10 9 fveq2d GVEW=EGsSetScalarndxringsSetndxG
11 7 10 eqtr4id GVEG=EW
12 2 str0 =E
13 12 eqcomi E=
14 13 1 fveqprc ¬GVEG=EW
15 11 14 pm2.61i EG=EW