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

Metamath Proof Explorer

Theorem issstrmgm

Description: Characterize a substructure as submagma by closure properties. (Contributed by AV, 30-Aug-2021)

Ref Expression
Hypotheses issstrmgm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
issstrmgm.p ⊢ + = ( +g ‘ 𝐺 )
issstrmgm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion issstrmgm ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐻 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 issstrmgm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 issstrmgm.p ⊢ + = ( +g ‘ 𝐺 )
3 issstrmgm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
4 simplr ⊢ ( ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐻 ∈ Mgm )
5 simplr ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → 𝑆 ⊆ 𝐵 )
6 3 1 ressbas2 ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ 𝐻 ) )
7 5 6 syl ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → 𝑆 = ( Base ‘ 𝐻 ) )
8 7 eleq2d ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → ( 𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
9 8 biimpcd ⊢ ( 𝑥 ∈ 𝑆 → ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
10 9 adantr ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
11 10 impcom ⊢ ( ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝐻 ) )
12 7 eleq2d ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → ( 𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
13 12 biimpcd ⊢ ( 𝑦 ∈ 𝑆 → ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
14 13 adantl ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
15 14 impcom ⊢ ( ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐻 ) )
16 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
17 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
18 16 17 mgmcl ⊢ ( ( 𝐻 ∈ Mgm ∧ 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
19 4 11 15 18 syl3anc ⊢ ( ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
20 1 fvexi ⊢ 𝐵 ∈ V
21 20 ssex ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ V )
22 21 adantl ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ V )
23 3 2 ressplusg ⊢ ( 𝑆 ∈ V → + = ( +g ‘ 𝐻 ) )
24 22 23 syl ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → + = ( +g ‘ 𝐻 ) )
25 24 adantr ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → + = ( +g ‘ 𝐻 ) )
26 25 oveqdr ⊢ ( ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
27 7 adantr ⊢ ( ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
28 19 26 27 3eltr4d ⊢ ( ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
29 28 ralrimivva ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝐻 ∈ Mgm ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
30 6 adantl ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 = ( Base ‘ 𝐻 ) )
31 24 oveqd ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
32 31 30 eleq12d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) ) )
33 30 32 raleqbidv ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) ) )
34 30 33 raleqbidv ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) ) )
35 34 biimpa ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
36 16 17 ismgm ⊢ ( 𝐻 ∈ 𝑉 → ( 𝐻 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) ) )
37 36 ad2antrr ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( 𝐻 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) ) )
38 35 37 mpbird ⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → 𝐻 ∈ Mgm )
39 29 38 impbida ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐻 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )