# 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 ) ) )