Metamath Proof Explorer


Theorem mgmsscl

Description: If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. Formerly part of proof of grpissubg . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses mgmsscl.b 𝐵 = ( Base ‘ 𝐺 )
mgmsscl.s 𝑆 = ( Base ‘ 𝐻 )
Assertion mgmsscl ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( 𝑋 ( +g𝐺 ) 𝑌 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 mgmsscl.b 𝐵 = ( Base ‘ 𝐺 )
2 mgmsscl.s 𝑆 = ( Base ‘ 𝐻 )
3 ovres ( ( 𝑋𝑆𝑌𝑆 ) → ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) = ( 𝑋 ( +g𝐺 ) 𝑌 ) )
4 3 3ad2ant3 ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) = ( 𝑋 ( +g𝐺 ) 𝑌 ) )
5 simp1r ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → 𝐻 ∈ Mgm )
6 simp3 ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( 𝑋𝑆𝑌𝑆 ) )
7 3anass ( ( 𝐻 ∈ Mgm ∧ 𝑋𝑆𝑌𝑆 ) ↔ ( 𝐻 ∈ Mgm ∧ ( 𝑋𝑆𝑌𝑆 ) ) )
8 5 6 7 sylanbrc ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( 𝐻 ∈ Mgm ∧ 𝑋𝑆𝑌𝑆 ) )
9 eqid ( +g𝐻 ) = ( +g𝐻 )
10 2 9 mgmcl ( ( 𝐻 ∈ Mgm ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑋 ( +g𝐻 ) 𝑌 ) ∈ 𝑆 )
11 8 10 syl ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( 𝑋 ( +g𝐻 ) 𝑌 ) ∈ 𝑆 )
12 oveq ( ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) = ( +g𝐻 ) → ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) = ( 𝑋 ( +g𝐻 ) 𝑌 ) )
13 12 eleq1d ( ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) = ( +g𝐻 ) → ( ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) ∈ 𝑆 ↔ ( 𝑋 ( +g𝐻 ) 𝑌 ) ∈ 𝑆 ) )
14 13 eqcoms ( ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) → ( ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) ∈ 𝑆 ↔ ( 𝑋 ( +g𝐻 ) 𝑌 ) ∈ 𝑆 ) )
15 14 adantl ( ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) ∈ 𝑆 ↔ ( 𝑋 ( +g𝐻 ) 𝑌 ) ∈ 𝑆 ) )
16 15 3ad2ant2 ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) ∈ 𝑆 ↔ ( 𝑋 ( +g𝐻 ) 𝑌 ) ∈ 𝑆 ) )
17 11 16 mpbird ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( 𝑋 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑌 ) ∈ 𝑆 )
18 4 17 eqeltrrd ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑋𝑆𝑌𝑆 ) ) → ( 𝑋 ( +g𝐺 ) 𝑌 ) ∈ 𝑆 )