Theorem issubmd 27251

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

Hypotheses

Ref	Expression
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

Ref	Expression
issubmd	|- ( ph -> { z e. B | ps } e. (SubMnd ` M ) )

Distinct variable groups:   x, y, z, B   x, M, y   ph, x, y   ps, x, y   z, .+   z, .0.   ch, z   et, z   ta, z   th, z

Allowed substitution hints:   ph( z)   ps( z)   ch( x, y)   th( x, y)   ta( x, y)   et( x, y)   .+ ( x, y)   M( z)   .0. ( x, y)

Proof of Theorem issubmd

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

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   {crab 2670   C_ wss 3280   ` cfv 5413  (class class class)co 6040   Basecbs 13424   +g cplusg 13484   0gc0g 13678   Mndcmnd 14639  SubMndcsubmnd 14692

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-ov 6043  df-riota 6508  df-0g 13682  df-mnd 14645  df-submnd 14694