Metamath Proof Explorer


Theorem 2zrngmmgm

Description: R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020)

Ref Expression
Hypotheses 2zrng.e E=z|xz=2x
2zrngbas.r R=fld𝑠E
2zrngmmgm.1 M=mulGrpR
Assertion 2zrngmmgm MMgm

Proof

Step Hyp Ref Expression
1 2zrng.e E=z|xz=2x
2 2zrngbas.r R=fld𝑠E
3 2zrngmmgm.1 M=mulGrpR
4 eqeq1 z=az=2xa=2x
5 4 rexbidv z=axz=2xxa=2x
6 5 1 elrab2 aEaxa=2x
7 eqeq1 z=bz=2xb=2x
8 7 rexbidv z=bxz=2xxb=2x
9 8 1 elrab2 bEbxb=2x
10 zmulcl abab
11 10 ad2ant2r axa=2xbxb=2xab
12 nfv xa
13 nfv xb
14 nfre1 xxb=2x
15 13 14 nfan xbxb=2x
16 nfv xyab=2y
17 15 16 nfim xbxb=2xyab=2y
18 12 17 nfim xabxb=2xyab=2y
19 simpll xa=2xax
20 simpl bxb=2xb
21 zmulcl xbxb
22 19 20 21 syl2an xa=2xabxb=2xxb
23 oveq2 y=xb2y=2xb
24 23 eqeq2d y=xbab=2yab=2xb
25 24 adantl xa=2xabxb=2xy=xbab=2yab=2xb
26 oveq1 a=2xab=2xb
27 26 ad3antlr xa=2xabxb=2xab=2xb
28 2cnd xa=2xabxb=2x2
29 zcn xx
30 29 ad3antrrr xa=2xabxb=2xx
31 zcn bb
32 31 adantr bxb=2xb
33 32 adantl xa=2xabxb=2xb
34 28 30 33 mulassd xa=2xabxb=2x2xb=2xb
35 27 34 eqtrd xa=2xabxb=2xab=2xb
36 22 25 35 rspcedvd xa=2xabxb=2xyab=2y
37 36 exp41 xa=2xabxb=2xyab=2y
38 18 37 rexlimi xa=2xabxb=2xyab=2y
39 38 impcom axa=2xbxb=2xyab=2y
40 39 imp axa=2xbxb=2xyab=2y
41 eqeq1 z=abz=2xab=2x
42 41 rexbidv z=abxz=2xxab=2x
43 42 1 elrab2 abEabxab=2x
44 oveq2 x=y2x=2y
45 44 eqeq2d x=yab=2xab=2y
46 45 cbvrexvw xab=2xyab=2y
47 46 anbi2i abxab=2xabyab=2y
48 43 47 bitri abEabyab=2y
49 11 40 48 sylanbrc axa=2xbxb=2xabE
50 6 9 49 syl2anb aEbEabE
51 50 rgen2 aEbEabE
52 1 0even 0E
53 1 2 2zrngbas E=BaseR
54 3 53 mgpbas E=BaseM
55 1 2 2zrngmul ×=R
56 3 55 mgpplusg ×=+M
57 54 56 ismgmn0 0EMMgmaEbEabE
58 52 57 ax-mp MMgmaEbEabE
59 51 58 mpbir MMgm