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

Metamath Proof Explorer

Theorem 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 ) ) )