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 ⊢ 𝐻 = ( 𝐺 ↾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 eqtrid ⊢ ( ( 𝑆 ∈ ( 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 ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) )