Metamath Proof Explorer

Theorem rabsubmgmd

Description: Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypotheses rabsubmgmd.b 
|- B = ( Base ` M )
rabsubmgmd.p 
|- .+ = ( +g ` M )
rabsubmgmd.m 
|- ( ph -> M e. Mgm )
rabsubmgmd.cp 
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) ) -> et )
rabsubmgmd.th 
|- ( z = x -> ( ps <-> th ) )
rabsubmgmd.ta 
|- ( z = y -> ( ps <-> ta ) )
rabsubmgmd.et 
|- ( z = ( x .+ y ) -> ( ps <-> et ) )
Assertion rabsubmgmd 
|- ( ph -> { z e. B | ps } e. ( SubMgm ` M ) )

Proof

Step Hyp Ref Expression
1 rabsubmgmd.b 
 |-  B = ( Base ` M )
2 rabsubmgmd.p 
 |-  .+ = ( +g ` M )
3 rabsubmgmd.m 
 |-  ( ph -> M e. Mgm )
4 rabsubmgmd.cp 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) ) -> et )
5 rabsubmgmd.th 
 |-  ( z = x -> ( ps <-> th ) )
6 rabsubmgmd.ta 
 |-  ( z = y -> ( ps <-> ta ) )
7 rabsubmgmd.et 
 |-  ( z = ( x .+ y ) -> ( ps <-> et ) )
8 ssrab2 
 |-  { z e. B | ps } C_ B
9 8 a1i 
 |-  ( ph -> { z e. B | ps } C_ B )
10 5 elrab 
 |-  ( x e. { z e. B | ps } <-> ( x e. B /\ th ) )
11 6 elrab 
 |-  ( y e. { z e. B | ps } <-> ( y e. B /\ ta ) )
12 10 11 anbi12i 
 |-  ( ( x e. { z e. B | ps } /\ y e. { z e. B | ps } ) <-> ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) )
13 3 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> M e. Mgm )
14 simprll 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> x e. B )
15 simprrl 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> y e. B )
16 1 2 mgmcl 
 |-  ( ( M e. Mgm /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
17 13 14 15 16 syl3anc 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> ( x .+ y ) e. B )
18 simpl 
 |-  ( ( x e. B /\ th ) -> x e. B )
19 simpl 
 |-  ( ( y e. B /\ ta ) -> y e. B )
20 18 19 anim12i 
 |-  ( ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) -> ( x e. B /\ y e. B ) )
21 simpr 
 |-  ( ( x e. B /\ th ) -> th )
22 simpr 
 |-  ( ( y e. B /\ ta ) -> ta )
23 21 22 anim12i 
 |-  ( ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) -> ( th /\ ta ) )
24 20 23 jca 
 |-  ( ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) -> ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) )
25 24 4 sylan2 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> et )
26 7 17 25 elrabd 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> ( x .+ y ) e. { z e. B | ps } )
27 12 26 sylan2b 
 |-  ( ( ph /\ ( x e. { z e. B | ps } /\ y e. { z e. B | ps } ) ) -> ( x .+ y ) e. { z e. B | ps } )
28 27 ralrimivva 
 |-  ( ph -> A. x e. { z e. B | ps } A. y e. { z e. B | ps } ( x .+ y ) e. { z e. B | ps } )
29 1 2 issubmgm 
 |-  ( M e. Mgm -> ( { z e. B | ps } e. ( SubMgm ` M ) <-> ( { z e. B | ps } C_ B /\ A. x e. { z e. B | ps } A. y e. { z e. B | ps } ( x .+ y ) e. { z e. B | ps } ) ) )
30 3 29 syl 
 |-  ( ph -> ( { z e. B | ps } e. ( SubMgm ` M ) <-> ( { z e. B | ps } C_ B /\ A. x e. { z e. B | ps } A. y e. { z e. B | ps } ( x .+ y ) e. { z e. B | ps } ) ) )
31 9 28 30 mpbir2and 
 |-  ( ph -> { z e. B | ps } e. ( SubMgm ` M ) )