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 ) ) )