# 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
`|- .+ = ( +g ` M )`
Assertion issubmgm
`|- ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )`

### Proof

Step Hyp Ref Expression
1 issubmgm.b
` |-  B = ( Base ` M )`
2 issubmgm.p
` |-  .+ = ( +g ` M )`
3 fveq2
` |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )`
4 3 pweqd
` |-  ( m = M -> ~P ( Base ` m ) = ~P ( Base ` M ) )`
5 fveq2
` |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )`
6 5 oveqd
` |-  ( m = M -> ( x ( +g ` m ) y ) = ( x ( +g ` M ) y ) )`
7 6 eleq1d
` |-  ( m = M -> ( ( x ( +g ` m ) y ) e. t <-> ( x ( +g ` M ) y ) e. t ) )`
8 7 2ralbidv
` |-  ( m = M -> ( A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t <-> A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) )`
9 4 8 rabeqbidv
` |-  ( m = M -> { t e. ~P ( Base ` m ) | A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t } = { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } )`
10 df-submgm
` |-  SubMgm = ( m e. Mgm |-> { t e. ~P ( Base ` m ) | A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t } )`
11 fvex
` |-  ( Base ` M ) e. _V`
12 11 pwex
` |-  ~P ( Base ` M ) e. _V`
13 12 rabex
` |-  { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } e. _V`
14 9 10 13 fvmpt
` |-  ( M e. Mgm -> ( SubMgm ` M ) = { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } )`
15 14 eleq2d
` |-  ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> S e. { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } ) )`
16 11 elpw2
` |-  ( S e. ~P ( Base ` M ) <-> S C_ ( Base ` M ) )`
17 16 anbi1i
` |-  ( ( S e. ~P ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) <-> ( S C_ ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) )`
18 eleq2
` |-  ( t = S -> ( ( x ( +g ` M ) y ) e. t <-> ( x ( +g ` M ) y ) e. S ) )`
19 18 raleqbi1dv
` |-  ( t = S -> ( A. y e. t ( x ( +g ` M ) y ) e. t <-> A. y e. S ( x ( +g ` M ) y ) e. S ) )`
20 19 raleqbi1dv
` |-  ( t = S -> ( A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t <-> A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) )`
21 20 elrab
` |-  ( S e. { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } <-> ( S e. ~P ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) )`
22 1 sseq2i
` |-  ( S C_ B <-> S C_ ( Base ` M ) )`
23 2 oveqi
` |-  ( x .+ y ) = ( x ( +g ` M ) y )`
24 23 eleq1i
` |-  ( ( x .+ y ) e. S <-> ( x ( +g ` M ) y ) e. S )`
25 24 2ralbii
` |-  ( A. x e. S A. y e. S ( x .+ y ) e. S <-> A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S )`
26 22 25 anbi12i
` |-  ( ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) <-> ( S C_ ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) )`
27 17 21 26 3bitr4i
` |-  ( S e. { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } <-> ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) )`
28 15 27 syl6bb
` |-  ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )`