Metamath Proof Explorer


Theorem issubm

Description: Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses issubm.b B=BaseM
issubm.z 0˙=0M
issubm.p +˙=+M
Assertion issubm MMndSSubMndMSB0˙SxSySx+˙yS

Proof

Step Hyp Ref Expression
1 issubm.b B=BaseM
2 issubm.z 0˙=0M
3 issubm.p +˙=+M
4 fveq2 m=MBasem=BaseM
5 4 pweqd m=M𝒫Basem=𝒫BaseM
6 fveq2 m=M0m=0M
7 6 eleq1d m=M0mt0Mt
8 fveq2 m=M+m=+M
9 8 oveqd m=Mx+my=x+My
10 9 eleq1d m=Mx+mytx+Myt
11 10 2ralbidv m=Mxtytx+mytxtytx+Myt
12 7 11 anbi12d m=M0mtxtytx+myt0Mtxtytx+Myt
13 5 12 rabeqbidv m=Mt𝒫Basem|0mtxtytx+myt=t𝒫BaseM|0Mtxtytx+Myt
14 df-submnd SubMnd=mMndt𝒫Basem|0mtxtytx+myt
15 fvex BaseMV
16 15 pwex 𝒫BaseMV
17 16 rabex t𝒫BaseM|0Mtxtytx+MytV
18 13 14 17 fvmpt MMndSubMndM=t𝒫BaseM|0Mtxtytx+Myt
19 18 eleq2d MMndSSubMndMSt𝒫BaseM|0Mtxtytx+Myt
20 eleq2 t=S0Mt0MS
21 eleq2 t=Sx+Mytx+MyS
22 21 raleqbi1dv t=Sytx+MytySx+MyS
23 22 raleqbi1dv t=Sxtytx+MytxSySx+MyS
24 20 23 anbi12d t=S0Mtxtytx+Myt0MSxSySx+MyS
25 24 elrab St𝒫BaseM|0Mtxtytx+MytS𝒫BaseM0MSxSySx+MyS
26 1 sseq2i SBSBaseM
27 2 eleq1i 0˙S0MS
28 3 oveqi x+˙y=x+My
29 28 eleq1i x+˙ySx+MyS
30 29 2ralbii xSySx+˙ySxSySx+MyS
31 27 30 anbi12i 0˙SxSySx+˙yS0MSxSySx+MyS
32 26 31 anbi12i SB0˙SxSySx+˙ySSBaseM0MSxSySx+MyS
33 3anass SB0˙SxSySx+˙ySSB0˙SxSySx+˙yS
34 15 elpw2 S𝒫BaseMSBaseM
35 34 anbi1i S𝒫BaseM0MSxSySx+MySSBaseM0MSxSySx+MyS
36 32 33 35 3bitr4ri S𝒫BaseM0MSxSySx+MySSB0˙SxSySx+˙yS
37 25 36 bitri St𝒫BaseM|0Mtxtytx+MytSB0˙SxSySx+˙yS
38 19 37 bitrdi MMndSSubMndMSB0˙SxSySx+˙yS