Metamath Proof Explorer


Theorem mulgaddcomlem

Description: Lemma for mulgaddcom . (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)

Ref Expression
Hypotheses mulgaddcom.b B=BaseG
mulgaddcom.t ·˙=G
mulgaddcom.p +˙=+G
Assertion mulgaddcomlem GGrpyXBy·˙X+˙X=X+˙y·˙Xy·˙X+˙X=X+˙y·˙X

Proof

Step Hyp Ref Expression
1 mulgaddcom.b B=BaseG
2 mulgaddcom.t ·˙=G
3 mulgaddcom.p +˙=+G
4 simp1 GGrpyXBGGrp
5 4 adantr GGrpyXBy·˙X+˙X=X+˙y·˙XGGrp
6 simp3 GGrpyXBXB
7 6 adantr GGrpyXBy·˙X+˙X=X+˙y·˙XXB
8 znegcl yy
9 1 2 mulgcl GGrpyXBy·˙XB
10 8 9 syl3an2 GGrpyXBy·˙XB
11 10 adantr GGrpyXBy·˙X+˙X=X+˙y·˙Xy·˙XB
12 eqid invgG=invgG
13 1 12 grpinvcl GGrpXBinvgGXB
14 13 3adant2 GGrpyXBinvgGXB
15 14 adantr GGrpyXBy·˙X+˙X=X+˙y·˙XinvgGXB
16 1 3 grpass GGrpXBy·˙XBinvgGXBX+˙y·˙X+˙invgGX=X+˙y·˙X+˙invgGX
17 5 7 11 15 16 syl13anc GGrpyXBy·˙X+˙X=X+˙y·˙XX+˙y·˙X+˙invgGX=X+˙y·˙X+˙invgGX
18 1 2 12 mulgneg GGrpyXBy·˙X=invgGy·˙X
19 18 adantr GGrpyXBy·˙X+˙X=X+˙y·˙Xy·˙X=invgGy·˙X
20 19 oveq1d GGrpyXBy·˙X+˙X=X+˙y·˙Xy·˙X+˙invgGX=invgGy·˙X+˙invgGX
21 1 2 mulgcl GGrpyXBy·˙XB
22 21 adantr GGrpyXBy·˙X+˙X=X+˙y·˙Xy·˙XB
23 1 3 12 grpinvadd GGrpXBy·˙XBinvgGX+˙y·˙X=invgGy·˙X+˙invgGX
24 5 7 22 23 syl3anc GGrpyXBy·˙X+˙X=X+˙y·˙XinvgGX+˙y·˙X=invgGy·˙X+˙invgGX
25 19 oveq2d GGrpyXBy·˙X+˙X=X+˙y·˙XinvgGX+˙y·˙X=invgGX+˙invgGy·˙X
26 1 3 12 grpinvadd GGrpy·˙XBXBinvgGy·˙X+˙X=invgGX+˙invgGy·˙X
27 5 22 7 26 syl3anc GGrpyXBy·˙X+˙X=X+˙y·˙XinvgGy·˙X+˙X=invgGX+˙invgGy·˙X
28 fveq2 y·˙X+˙X=X+˙y·˙XinvgGy·˙X+˙X=invgGX+˙y·˙X
29 28 adantl GGrpyXBy·˙X+˙X=X+˙y·˙XinvgGy·˙X+˙X=invgGX+˙y·˙X
30 25 27 29 3eqtr2rd GGrpyXBy·˙X+˙X=X+˙y·˙XinvgGX+˙y·˙X=invgGX+˙y·˙X
31 20 24 30 3eqtr2d GGrpyXBy·˙X+˙X=X+˙y·˙Xy·˙X+˙invgGX=invgGX+˙y·˙X
32 31 oveq2d GGrpyXBy·˙X+˙X=X+˙y·˙XX+˙y·˙X+˙invgGX=X+˙invgGX+˙y·˙X
33 1 3 12 grpasscan1 GGrpXBy·˙XBX+˙invgGX+˙y·˙X=y·˙X
34 5 7 11 33 syl3anc GGrpyXBy·˙X+˙X=X+˙y·˙XX+˙invgGX+˙y·˙X=y·˙X
35 17 32 34 3eqtrd GGrpyXBy·˙X+˙X=X+˙y·˙XX+˙y·˙X+˙invgGX=y·˙X
36 35 oveq1d GGrpyXBy·˙X+˙X=X+˙y·˙XX+˙y·˙X+˙invgGX+˙X=y·˙X+˙X
37 1 3 grpcl GGrpXBy·˙XBX+˙y·˙XB
38 4 6 10 37 syl3anc GGrpyXBX+˙y·˙XB
39 38 adantr GGrpyXBy·˙X+˙X=X+˙y·˙XX+˙y·˙XB
40 1 3 12 grpasscan2 GGrpX+˙y·˙XBXBX+˙y·˙X+˙invgGX+˙X=X+˙y·˙X
41 5 39 7 40 syl3anc GGrpyXBy·˙X+˙X=X+˙y·˙XX+˙y·˙X+˙invgGX+˙X=X+˙y·˙X
42 36 41 eqtr3d GGrpyXBy·˙X+˙X=X+˙y·˙Xy·˙X+˙X=X+˙y·˙X