This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issubmd

Description: Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses issubmd.b 
|- B = ( Base ` M )
issubmd.p 
|- .+ = ( +g ` M )
issubmd.z 
|- .0. = ( 0g ` M )
issubmd.m 
|- ( ph -> M e. Mnd )
issubmd.cz 
|- ( ph -> ch )
issubmd.cp 
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) ) -> et )
issubmd.ch 
|- ( z = .0. -> ( ps <-> ch ) )
issubmd.th 
|- ( z = x -> ( ps <-> th ) )
issubmd.ta 
|- ( z = y -> ( ps <-> ta ) )
issubmd.et 
|- ( z = ( x .+ y ) -> ( ps <-> et ) )
Assertion issubmd 
|- ( ph -> { z e. B | ps } e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 issubmd.b 
 |-  B = ( Base ` M )
2 issubmd.p 
 |-  .+ = ( +g ` M )
3 issubmd.z 
 |-  .0. = ( 0g ` M )
4 issubmd.m 
 |-  ( ph -> M e. Mnd )
5 issubmd.cz 
 |-  ( ph -> ch )
6 issubmd.cp 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) ) -> et )
7 issubmd.ch 
 |-  ( z = .0. -> ( ps <-> ch ) )
8 issubmd.th 
 |-  ( z = x -> ( ps <-> th ) )
9 issubmd.ta 
 |-  ( z = y -> ( ps <-> ta ) )
10 issubmd.et 
 |-  ( z = ( x .+ y ) -> ( ps <-> et ) )
11 ssrab2 
 |-  { z e. B | ps } C_ B
12 11 a1i 
 |-  ( ph -> { z e. B | ps } C_ B )
13 1 3 mndidcl 
 |-  ( M e. Mnd -> .0. e. B )
14 4 13 syl 
 |-  ( ph -> .0. e. B )
15 7 14 5 elrabd 
 |-  ( ph -> .0. e. { z e. B | ps } )
16 8 elrab 
 |-  ( x e. { z e. B | ps } <-> ( x e. B /\ th ) )
17 9 elrab 
 |-  ( y e. { z e. B | ps } <-> ( y e. B /\ ta ) )
18 16 17 anbi12i 
 |-  ( ( x e. { z e. B | ps } /\ y e. { z e. B | ps } ) <-> ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) )
19 4 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> M e. Mnd )
20 simprll 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> x e. B )
21 simprrl 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> y e. B )
22 1 2 mndcl 
 |-  ( ( M e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
23 19 20 21 22 syl3anc 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> ( x .+ y ) e. B )
24 an4 
 |-  ( ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) <-> ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) )
25 24 6 sylan2b 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> et )
26 10 23 25 elrabd 
 |-  ( ( ph /\ ( ( x e. B /\ th ) /\ ( y e. B /\ ta ) ) ) -> ( x .+ y ) e. { z e. B | ps } )
27 18 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 3 2 issubm 
 |-  ( M e. Mnd -> ( { z e. B | ps } e. ( SubMnd ` M ) <-> ( { z e. B | ps } C_ B /\ .0. e. { z e. B | ps } /\ A. x e. { z e. B | ps } A. y e. { z e. B | ps } ( x .+ y ) e. { z e. B | ps } ) ) )
30 4 29 syl 
 |-  ( ph -> ( { z e. B | ps } e. ( SubMnd ` M ) <-> ( { z e. B | ps } C_ B /\ .0. e. { z e. B | ps } /\ A. x e. { z e. B | ps } A. y e. { z e. B | ps } ( x .+ y ) e. { z e. B | ps } ) ) )
31 12 15 28 30 mpbir3and 
 |-  ( ph -> { z e. B | ps } e. ( SubMnd ` M ) )