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

Metamath Proof Explorer

Theorem subsubm

Description: A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Hypothesis subsubm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion subsubm ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ↔ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 subsubm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
2 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
3 2 submss ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝐻 ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
4 3 adantl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
5 1 submbas ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
6 5 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
7 4 6 sseqtrrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → 𝐴 ⊆ 𝑆 )
8 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
9 8 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
10 9 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
11 7 10 sstrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
12 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
13 1 12 subm0 ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
14 13 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
15 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
16 15 subm0cl ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝐻 ) → ( 0g ‘ 𝐻 ) ∈ 𝐴 )
17 16 adantl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 0g ‘ 𝐻 ) ∈ 𝐴 )
18 14 17 eqeltrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝐴 )
19 1 oveq1i ⊢ ( 𝐻 ↾s 𝐴 ) = ( ( 𝐺 ↾s 𝑆 ) ↾s 𝐴 )
20 ressabs ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) → ( ( 𝐺 ↾s 𝑆 ) ↾s 𝐴 ) = ( 𝐺 ↾s 𝐴 ) )
21 19 20 eqtrid ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐻 ↾s 𝐴 ) = ( 𝐺 ↾s 𝐴 ) )
22 7 21 syldan ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 𝐻 ↾s 𝐴 ) = ( 𝐺 ↾s 𝐴 ) )
23 eqid ⊢ ( 𝐻 ↾s 𝐴 ) = ( 𝐻 ↾s 𝐴 )
24 23 submmnd ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝐻 ) → ( 𝐻 ↾s 𝐴 ) ∈ Mnd )
25 24 adantl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 𝐻 ↾s 𝐴 ) ∈ Mnd )
26 22 25 eqeltrrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 𝐺 ↾s 𝐴 ) ∈ Mnd )
27 submrcl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd )
28 27 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → 𝐺 ∈ Mnd )
29 eqid ⊢ ( 𝐺 ↾s 𝐴 ) = ( 𝐺 ↾s 𝐴 )
30 8 12 29 issubm2 ⊢ ( 𝐺 ∈ Mnd → ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝐴 ∧ ( 𝐺 ↾s 𝐴 ) ∈ Mnd ) ) )
31 28 30 syl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝐴 ∧ ( 𝐺 ↾s 𝐴 ) ∈ Mnd ) ) )
32 11 18 26 31 mpbir3and ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → 𝐴 ∈ ( SubMnd ‘ 𝐺 ) )
33 32 7 jca ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ) → ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) )
34 simprr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐴 ⊆ 𝑆 )
35 5 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
36 34 35 sseqtrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
37 13 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
38 12 subm0cl ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝐴 )
39 38 ad2antrl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝐴 )
40 37 39 eqeltrrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → ( 0g ‘ 𝐻 ) ∈ 𝐴 )
41 21 adantrl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → ( 𝐻 ↾s 𝐴 ) = ( 𝐺 ↾s 𝐴 ) )
42 29 submmnd ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐺 ↾s 𝐴 ) ∈ Mnd )
43 42 ad2antrl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → ( 𝐺 ↾s 𝐴 ) ∈ Mnd )
44 41 43 eqeltrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → ( 𝐻 ↾s 𝐴 ) ∈ Mnd )
45 1 submmnd ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐻 ∈ Mnd )
46 45 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐻 ∈ Mnd )
47 2 15 23 issubm2 ⊢ ( 𝐻 ∈ Mnd → ( 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐻 ) ∧ ( 0g ‘ 𝐻 ) ∈ 𝐴 ∧ ( 𝐻 ↾s 𝐴 ) ∈ Mnd ) ) )
48 46 47 syl ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → ( 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝐻 ) ∧ ( 0g ‘ 𝐻 ) ∈ 𝐴 ∧ ( 𝐻 ↾s 𝐴 ) ∈ Mnd ) ) )
49 36 40 44 48 mpbir3and ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐴 ∈ ( SubMnd ‘ 𝐻 ) )
50 33 49 impbida ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐴 ∈ ( SubMnd ‘ 𝐻 ) ↔ ( 𝐴 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) )