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

Metamath Proof Explorer

Theorem subsubmgm

Description: A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis subsubmgm.h 
|- H = ( G |`s S )
Assertion subsubmgm 
|- ( S e. ( SubMgm ` G ) -> ( A e. ( SubMgm ` H ) <-> ( A e. ( SubMgm ` G ) /\ A C_ S ) ) )

Proof

Step Hyp Ref Expression
1 subsubmgm.h 
 |-  H = ( G |`s S )
2 eqid 
 |-  ( Base ` H ) = ( Base ` H )
3 2 submgmss 
 |-  ( A e. ( SubMgm ` H ) -> A C_ ( Base ` H ) )
4 3 adantl 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> A C_ ( Base ` H ) )
5 1 submgmbas 
 |-  ( S e. ( SubMgm ` G ) -> S = ( Base ` H ) )
6 5 adantr 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> S = ( Base ` H ) )
7 4 6 sseqtrrd 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> A C_ S )
8 eqid 
 |-  ( Base ` G ) = ( Base ` G )
9 8 submgmss 
 |-  ( S e. ( SubMgm ` G ) -> S C_ ( Base ` G ) )
10 9 adantr 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> S C_ ( Base ` G ) )
11 7 10 sstrd 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> A C_ ( Base ` G ) )
12 1 oveq1i 
 |-  ( H |`s A ) = ( ( G |`s S ) |`s A )
13 ressabs 
 |-  ( ( S e. ( SubMgm ` G ) /\ A C_ S ) -> ( ( G |`s S ) |`s A ) = ( G |`s A ) )
14 12 13 eqtrid 
 |-  ( ( S e. ( SubMgm ` G ) /\ A C_ S ) -> ( H |`s A ) = ( G |`s A ) )
15 7 14 syldan 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> ( H |`s A ) = ( G |`s A ) )
16 eqid 
 |-  ( H |`s A ) = ( H |`s A )
17 16 submgmmgm 
 |-  ( A e. ( SubMgm ` H ) -> ( H |`s A ) e. Mgm )
18 17 adantl 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> ( H |`s A ) e. Mgm )
19 15 18 eqeltrrd 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> ( G |`s A ) e. Mgm )
20 submgmrcl 
 |-  ( S e. ( SubMgm ` G ) -> G e. Mgm )
21 20 adantr 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> G e. Mgm )
22 eqid 
 |-  ( G |`s A ) = ( G |`s A )
23 8 22 issubmgm2 
 |-  ( G e. Mgm -> ( A e. ( SubMgm ` G ) <-> ( A C_ ( Base ` G ) /\ ( G |`s A ) e. Mgm ) ) )
24 21 23 syl 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> ( A e. ( SubMgm ` G ) <-> ( A C_ ( Base ` G ) /\ ( G |`s A ) e. Mgm ) ) )
25 11 19 24 mpbir2and 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> A e. ( SubMgm ` G ) )
26 25 7 jca 
 |-  ( ( S e. ( SubMgm ` G ) /\ A e. ( SubMgm ` H ) ) -> ( A e. ( SubMgm ` G ) /\ A C_ S ) )
27 simprr 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> A C_ S )
28 5 adantr 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> S = ( Base ` H ) )
29 27 28 sseqtrd 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> A C_ ( Base ` H ) )
30 14 adantrl 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> ( H |`s A ) = ( G |`s A ) )
31 22 submgmmgm 
 |-  ( A e. ( SubMgm ` G ) -> ( G |`s A ) e. Mgm )
32 31 ad2antrl 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> ( G |`s A ) e. Mgm )
33 30 32 eqeltrd 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> ( H |`s A ) e. Mgm )
34 1 submgmmgm 
 |-  ( S e. ( SubMgm ` G ) -> H e. Mgm )
35 34 adantr 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> H e. Mgm )
36 2 16 issubmgm2 
 |-  ( H e. Mgm -> ( A e. ( SubMgm ` H ) <-> ( A C_ ( Base ` H ) /\ ( H |`s A ) e. Mgm ) ) )
37 35 36 syl 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> ( A e. ( SubMgm ` H ) <-> ( A C_ ( Base ` H ) /\ ( H |`s A ) e. Mgm ) ) )
38 29 33 37 mpbir2and 
 |-  ( ( S e. ( SubMgm ` G ) /\ ( A e. ( SubMgm ` G ) /\ A C_ S ) ) -> A e. ( SubMgm ` H ) )
39 26 38 impbida 
 |-  ( S e. ( SubMgm ` G ) -> ( A e. ( SubMgm ` H ) <-> ( A e. ( SubMgm ` G ) /\ A C_ S ) ) )