Metamath Proof Explorer

Theorem issubmgm2

Description: Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses issubmgm2.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
issubmgm2.h ⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
Assertion issubmgm2 ( 𝑀 ∈ Mgm → ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm ) ) )

Proof

Step Hyp Ref Expression
1 issubmgm2.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 issubmgm2.h ⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
3 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
4 1 3 issubmgm ⊢ ( 𝑀 ∈ Mgm → ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) ) )
5 2 1 ressbas2 ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ 𝐻 ) )
6 5 ad2antlr ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) → 𝑆 = ( Base ‘ 𝐻 ) )
7 ovex ⊢ ( 𝑀 ↾s 𝑆 ) ∈ V
8 2 7 eqeltri ⊢ 𝐻 ∈ V
9 8 a1i ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) → 𝐻 ∈ V )
10 1 fvexi ⊢ 𝐵 ∈ V
11 10 ssex ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ V )
12 11 ad2antlr ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) → 𝑆 ∈ V )
13 2 3 ressplusg ⊢ ( 𝑆 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ 𝐻 ) )
14 12 13 syl ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) → ( +g ‘ 𝑀 ) = ( +g ‘ 𝐻 ) )
15 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑦 ) )
16 15 eleq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ↔ ( 𝑎 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) )
17 oveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) )
18 17 eleq1d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ↔ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝑆 ) )
19 16 18 rspc2v ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝑆 ) )
20 19 com12 ⊢ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 → ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝑆 ) )
21 20 adantl ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) → ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝑆 ) )
22 21 3impib ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝑆 )
23 6 9 14 22 ismgmd ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) → 𝐻 ∈ Mgm )
24 simplr ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐻 ∈ Mgm )
25 simprl ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ 𝑆 )
26 5 ad3antlr ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
27 25 26 eleqtrd ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝐻 ) )
28 simpr ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
29 28 adantl ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
30 29 26 eleqtrd ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐻 ) )
31 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
32 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
33 31 32 mgmcl ⊢ ( ( 𝐻 ∈ Mgm ∧ 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
34 24 27 30 33 syl3anc ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
35 11 ad2antlr ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → 𝑆 ∈ V )
36 35 13 syl ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → ( +g ‘ 𝑀 ) = ( +g ‘ 𝐻 ) )
37 36 oveqdr ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
38 34 37 26 3eltr4d ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 )
39 38 ralrimivva ⊢ ( ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 )
40 23 39 impbida ⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ↔ 𝐻 ∈ Mgm ) )
41 40 pm5.32da ⊢ ( 𝑀 ∈ Mgm → ( ( 𝑆 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝑆 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm ) ) )
42 4 41 bitrd ⊢ ( 𝑀 ∈ Mgm → ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm ) ) )