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. = ( 0g ` M )
issubm.p 
|- .+ = ( +g ` M )
Assertion issubm 
|- ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )

Proof

Step Hyp Ref Expression
1 issubm.b 
 |-  B = ( Base ` M )
2 issubm.z 
 |-  .0. = ( 0g ` M )
3 issubm.p 
 |-  .+ = ( +g ` M )
4 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
5 4 pweqd 
 |-  ( m = M -> ~P ( Base ` m ) = ~P ( Base ` M ) )
6 fveq2 
 |-  ( m = M -> ( 0g ` m ) = ( 0g ` M ) )
7 6 eleq1d 
 |-  ( m = M -> ( ( 0g ` m ) e. t <-> ( 0g ` M ) e. t ) )
8 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
9 8 oveqd 
 |-  ( m = M -> ( x ( +g ` m ) y ) = ( x ( +g ` M ) y ) )
10 9 eleq1d 
 |-  ( m = M -> ( ( x ( +g ` m ) y ) e. t <-> ( x ( +g ` M ) y ) e. t ) )
11 10 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 ) )
12 7 11 anbi12d 
 |-  ( m = M -> ( ( ( 0g ` m ) e. t /\ A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t ) <-> ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) ) )
13 5 12 rabeqbidv 
 |-  ( m = M -> { t e. ~P ( Base ` m ) | ( ( 0g ` m ) e. t /\ A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t ) } = { t e. ~P ( Base ` M ) | ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) } )
14 df-submnd 
 |-  SubMnd = ( m e. Mnd |-> { t e. ~P ( Base ` m ) | ( ( 0g ` m ) e. t /\ A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t ) } )
15 fvex 
 |-  ( Base ` M ) e. _V
16 15 pwex 
 |-  ~P ( Base ` M ) e. _V
17 16 rabex 
 |-  { t e. ~P ( Base ` M ) | ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) } e. _V
18 13 14 17 fvmpt 
 |-  ( M e. Mnd -> ( SubMnd ` M ) = { t e. ~P ( Base ` M ) | ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) } )
19 18 eleq2d 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> S e. { t e. ~P ( Base ` M ) | ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) } ) )
20 eleq2 
 |-  ( t = S -> ( ( 0g ` M ) e. t <-> ( 0g ` M ) e. S ) )
21 eleq2 
 |-  ( t = S -> ( ( x ( +g ` M ) y ) e. t <-> ( x ( +g ` M ) y ) e. S ) )
22 21 raleqbi1dv 
 |-  ( t = S -> ( A. y e. t ( x ( +g ` M ) y ) e. t <-> A. y e. S ( x ( +g ` M ) y ) e. S ) )
23 22 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 ) )
24 20 23 anbi12d 
 |-  ( t = S -> ( ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) <-> ( ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) )
25 24 elrab 
 |-  ( S e. { t e. ~P ( Base ` M ) | ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) } <-> ( S e. ~P ( Base ` M ) /\ ( ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) )
26 1 sseq2i 
 |-  ( S C_ B <-> S C_ ( Base ` M ) )
27 2 eleq1i 
 |-  ( .0. e. S <-> ( 0g ` M ) e. S )
28 3 oveqi 
 |-  ( x .+ y ) = ( x ( +g ` M ) y )
29 28 eleq1i 
 |-  ( ( x .+ y ) e. S <-> ( x ( +g ` M ) y ) e. S )
30 29 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 )
31 27 30 anbi12i 
 |-  ( ( .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) <-> ( ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) )
32 26 31 anbi12i 
 |-  ( ( S C_ B /\ ( .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) <-> ( S C_ ( Base ` M ) /\ ( ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) )
33 3anass 
 |-  ( ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) <-> ( S C_ B /\ ( .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )
34 15 elpw2 
 |-  ( S e. ~P ( Base ` M ) <-> S C_ ( Base ` M ) )
35 34 anbi1i 
 |-  ( ( S e. ~P ( Base ` M ) /\ ( ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) <-> ( S C_ ( Base ` M ) /\ ( ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) )
36 32 33 35 3bitr4ri 
 |-  ( ( S e. ~P ( Base ` M ) /\ ( ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) <-> ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) )
37 25 36 bitri 
 |-  ( S e. { t e. ~P ( Base ` M ) | ( ( 0g ` M ) e. t /\ A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) } <-> ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) )
38 19 37 bitrdi 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )