Metamath Proof Explorer


Theorem issubmgm

Description: Expand definition of a submagma. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses issubmgm.b B = Base M
issubmgm.p + ˙ = + M
Assertion issubmgm M Mgm S SubMgm M S B x S y S x + ˙ y S

Proof

Step Hyp Ref Expression
1 issubmgm.b B = Base M
2 issubmgm.p + ˙ = + M
3 fveq2 m = M Base m = Base M
4 3 pweqd m = M 𝒫 Base m = 𝒫 Base M
5 fveq2 m = M + m = + M
6 5 oveqd m = M x + m y = x + M y
7 6 eleq1d m = M x + m y t x + M y t
8 7 2ralbidv m = M x t y t x + m y t x t y t x + M y t
9 4 8 rabeqbidv m = M t 𝒫 Base m | x t y t x + m y t = t 𝒫 Base M | x t y t x + M y t
10 df-submgm SubMgm = m Mgm t 𝒫 Base m | x t y t x + m y t
11 fvex Base M V
12 11 pwex 𝒫 Base M V
13 12 rabex t 𝒫 Base M | x t y t x + M y t V
14 9 10 13 fvmpt M Mgm SubMgm M = t 𝒫 Base M | x t y t x + M y t
15 14 eleq2d M Mgm S SubMgm M S t 𝒫 Base M | x t y t x + M y t
16 11 elpw2 S 𝒫 Base M S Base M
17 16 anbi1i S 𝒫 Base M x S y S x + M y S S Base M x S y S x + M y S
18 eleq2 t = S x + M y t x + M y S
19 18 raleqbi1dv t = S y t x + M y t y S x + M y S
20 19 raleqbi1dv t = S x t y t x + M y t x S y S x + M y S
21 20 elrab S t 𝒫 Base M | x t y t x + M y t S 𝒫 Base M x S y S x + M y S
22 1 sseq2i S B S Base M
23 2 oveqi x + ˙ y = x + M y
24 23 eleq1i x + ˙ y S x + M y S
25 24 2ralbii x S y S x + ˙ y S x S y S x + M y S
26 22 25 anbi12i S B x S y S x + ˙ y S S Base M x S y S x + M y S
27 17 21 26 3bitr4i S t 𝒫 Base M | x t y t x + M y t S B x S y S x + ˙ y S
28 15 27 bitrdi M Mgm S SubMgm M S B x S y S x + ˙ y S