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 𝐻 = ( 𝐺s 𝑆 )
Assertion subsubmgm ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) → ( 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ↔ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 subsubmgm.h 𝐻 = ( 𝐺s 𝑆 )
2 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
3 2 submgmss ( 𝐴 ∈ ( SubMgm ‘ 𝐻 ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
4 3 adantl ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
5 1 submgmbas ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
6 5 adantr ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
7 4 6 sseqtrrd ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → 𝐴𝑆 )
8 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
9 8 submgmss ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
10 9 adantr ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
11 7 10 sstrd ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
12 1 oveq1i ( 𝐻s 𝐴 ) = ( ( 𝐺s 𝑆 ) ↾s 𝐴 )
13 ressabs ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) → ( ( 𝐺s 𝑆 ) ↾s 𝐴 ) = ( 𝐺s 𝐴 ) )
14 12 13 syl5eq ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) → ( 𝐻s 𝐴 ) = ( 𝐺s 𝐴 ) )
15 7 14 syldan ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → ( 𝐻s 𝐴 ) = ( 𝐺s 𝐴 ) )
16 eqid ( 𝐻s 𝐴 ) = ( 𝐻s 𝐴 )
17 16 submgmmgm ( 𝐴 ∈ ( SubMgm ‘ 𝐻 ) → ( 𝐻s 𝐴 ) ∈ Mgm )
18 17 adantl ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → ( 𝐻s 𝐴 ) ∈ Mgm )
19 15 18 eqeltrrd ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → ( 𝐺s 𝐴 ) ∈ Mgm )
20 submgmrcl ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) → 𝐺 ∈ Mgm )
21 20 adantr ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → 𝐺 ∈ Mgm )
22 eqid ( 𝐺s 𝐴 ) = ( 𝐺s 𝐴 )
23 8 22 issubmgm2 ( 𝐺 ∈ Mgm → ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺s 𝐴 ) ∈ Mgm ) ) )
24 21 23 syl ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺s 𝐴 ) ∈ Mgm ) ) )
25 11 19 24 mpbir2and ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → 𝐴 ∈ ( SubMgm ‘ 𝐺 ) )
26 25 7 jca ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ) → ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) )
27 simprr ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐴𝑆 )
28 5 adantr ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
29 27 28 sseqtrd ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
30 14 adantrl ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → ( 𝐻s 𝐴 ) = ( 𝐺s 𝐴 ) )
31 22 submgmmgm ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) → ( 𝐺s 𝐴 ) ∈ Mgm )
32 31 ad2antrl ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → ( 𝐺s 𝐴 ) ∈ Mgm )
33 30 32 eqeltrd ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → ( 𝐻s 𝐴 ) ∈ Mgm )
34 1 submgmmgm ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) → 𝐻 ∈ Mgm )
35 34 adantr ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐻 ∈ Mgm )
36 2 16 issubmgm2 ( 𝐻 ∈ Mgm → ( 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐻 ) ∧ ( 𝐻s 𝐴 ) ∈ Mgm ) ) )
37 35 36 syl ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → ( 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐻 ) ∧ ( 𝐻s 𝐴 ) ∈ Mgm ) ) )
38 29 33 37 mpbir2and ( ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐴 ∈ ( SubMgm ‘ 𝐻 ) )
39 26 38 impbida ( 𝑆 ∈ ( SubMgm ‘ 𝐺 ) → ( 𝐴 ∈ ( SubMgm ‘ 𝐻 ) ↔ ( 𝐴 ∈ ( SubMgm ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) )