Metamath Proof Explorer


Theorem issubm

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

Ref Expression
Hypotheses issubm.b B = Base M
issubm.z 0 ˙ = 0 M
issubm.p + ˙ = + M
Assertion issubm M Mnd S SubMnd M S B 0 ˙ S x S y S x + ˙ y S

Proof

Step Hyp Ref Expression
1 issubm.b B = Base M
2 issubm.z 0 ˙ = 0 M
3 issubm.p + ˙ = + M
4 fveq2 m = M Base m = Base M
5 4 pweqd m = M 𝒫 Base m = 𝒫 Base M
6 fveq2 m = M 0 m = 0 M
7 6 eleq1d m = M 0 m t 0 M t
8 fveq2 m = M + m = + M
9 8 oveqd m = M x + m y = x + M y
10 9 eleq1d m = M x + m y t x + M y t
11 10 2ralbidv m = M x t y t x + m y t x t y t x + M y t
12 7 11 anbi12d m = M 0 m t x t y t x + m y t 0 M t x t y t x + M y t
13 5 12 rabeqbidv m = M t 𝒫 Base m | 0 m t x t y t x + m y t = t 𝒫 Base M | 0 M t x t y t x + M y t
14 df-submnd SubMnd = m Mnd t 𝒫 Base m | 0 m t x t y t x + m y t
15 fvex Base M V
16 15 pwex 𝒫 Base M V
17 16 rabex t 𝒫 Base M | 0 M t x t y t x + M y t V
18 13 14 17 fvmpt M Mnd SubMnd M = t 𝒫 Base M | 0 M t x t y t x + M y t
19 18 eleq2d M Mnd S SubMnd M S t 𝒫 Base M | 0 M t x t y t x + M y t
20 eleq2 t = S 0 M t 0 M S
21 eleq2 t = S x + M y t x + M y S
22 21 raleqbi1dv t = S y t x + M y t y S x + M y S
23 22 raleqbi1dv t = S x t y t x + M y t x S y S x + M y S
24 20 23 anbi12d t = S 0 M t x t y t x + M y t 0 M S x S y S x + M y S
25 24 elrab S t 𝒫 Base M | 0 M t x t y t x + M y t S 𝒫 Base M 0 M S x S y S x + M y S
26 1 sseq2i S B S Base M
27 2 eleq1i 0 ˙ S 0 M S
28 3 oveqi x + ˙ y = x + M y
29 28 eleq1i x + ˙ y S x + M y S
30 29 2ralbii x S y S x + ˙ y S x S y S x + M y S
31 27 30 anbi12i 0 ˙ S x S y S x + ˙ y S 0 M S x S y S x + M y S
32 26 31 anbi12i S B 0 ˙ S x S y S x + ˙ y S S Base M 0 M S x S y S x + M y S
33 3anass S B 0 ˙ S x S y S x + ˙ y S S B 0 ˙ S x S y S x + ˙ y S
34 15 elpw2 S 𝒫 Base M S Base M
35 34 anbi1i S 𝒫 Base M 0 M S x S y S x + M y S S Base M 0 M S x S y S x + M y S
36 32 33 35 3bitr4ri S 𝒫 Base M 0 M S x S y S x + M y S S B 0 ˙ S x S y S x + ˙ y S
37 25 36 bitri S t 𝒫 Base M | 0 M t x t y t x + M y t S B 0 ˙ S x S y S x + ˙ y S
38 19 37 bitrdi M Mnd S SubMnd M S B 0 ˙ S x S y S x + ˙ y S