issubmgm2

Description: Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	issubmgm2.b	\|- B = ( Base ` M )
	issubmgm2.h	\|- H = ( M \|`s S )
Assertion	issubmgm2	\|- ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ H e. Mgm ) ) )

Proof

Step	Hyp	Ref	Expression
1		issubmgm2.b	\|- B = ( Base ` M )
2		issubmgm2.h	\|- H = ( M \|`s S )
3		eqid	\|- ( +g ` M ) = ( +g ` M )
4	1 3	issubmgm	\|- ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) )
5	2 1	ressbas2	\|- ( S C_ B -> S = ( Base ` H ) )
6	5	ad2antlr	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) -> S = ( Base ` H ) )
7		ovex	\|- ( M \|`s S ) e. _V
8	2 7	eqeltri	\|- H e. _V
9	8	a1i	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) -> H e. _V )
10	1	fvexi	\|- B e. _V
11	10	ssex	\|- ( S C_ B -> S e. _V )
12	11	ad2antlr	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) -> S e. _V )
13	2 3	ressplusg	\|- ( S e. _V -> ( +g ` M ) = ( +g ` H ) )
14	12 13	syl	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) -> ( +g ` M ) = ( +g ` H ) )
15		oveq1	\|- ( x = a -> ( x ( +g ` M ) y ) = ( a ( +g ` M ) y ) )
16	15	eleq1d	\|- ( x = a -> ( ( x ( +g ` M ) y ) e. S <-> ( a ( +g ` M ) y ) e. S ) )
17		oveq2	\|- ( y = b -> ( a ( +g ` M ) y ) = ( a ( +g ` M ) b ) )
18	17	eleq1d	\|- ( y = b -> ( ( a ( +g ` M ) y ) e. S <-> ( a ( +g ` M ) b ) e. S ) )
19	16 18	rspc2v	\|- ( ( a e. S /\ b e. S ) -> ( A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S -> ( a ( +g ` M ) b ) e. S ) )
20	19	com12	\|- ( A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S -> ( ( a e. S /\ b e. S ) -> ( a ( +g ` M ) b ) e. S ) )
21	20	adantl	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) -> ( ( a e. S /\ b e. S ) -> ( a ( +g ` M ) b ) e. S ) )
22	21	3impib	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) /\ a e. S /\ b e. S ) -> ( a ( +g ` M ) b ) e. S )
23	6 9 14 22	ismgmd	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) -> H e. Mgm )
24		simplr	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> H e. Mgm )
25		simprl	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> x e. S )
26	5	ad3antlr	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> S = ( Base ` H ) )
27	25 26	eleqtrd	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> x e. ( Base ` H ) )
28		simpr	\|- ( ( x e. S /\ y e. S ) -> y e. S )
29	28	adantl	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> y e. S )
30	29 26	eleqtrd	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> y e. ( Base ` H ) )
31		eqid	\|- ( Base ` H ) = ( Base ` H )
32		eqid	\|- ( +g ` H ) = ( +g ` H )
33	31 32	mgmcl	\|- ( ( H e. Mgm /\ x e. ( Base ` H ) /\ y e. ( Base ` H ) ) -> ( x ( +g ` H ) y ) e. ( Base ` H ) )
34	24 27 30 33	syl3anc	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` H ) y ) e. ( Base ` H ) )
35	11	ad2antlr	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) -> S e. _V )
36	35 13	syl	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) -> ( +g ` M ) = ( +g ` H ) )
37	36	oveqdr	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` M ) y ) = ( x ( +g ` H ) y ) )
38	34 37 26	3eltr4d	\|- ( ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` M ) y ) e. S )
39	38	ralrimivva	\|- ( ( ( M e. Mgm /\ S C_ B ) /\ H e. Mgm ) -> A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S )
40	23 39	impbida	\|- ( ( M e. Mgm /\ S C_ B ) -> ( A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S <-> H e. Mgm ) )
41	40	pm5.32da	\|- ( M e. Mgm -> ( ( S C_ B /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) <-> ( S C_ B /\ H e. Mgm ) ) )
42	4 41	bitrd	\|- ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ H e. Mgm ) ) )

Metamath Proof Explorer

Theorem issubmgm2

Proof