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 ‘ 𝐺 ) 𝑌 ) ∈ 𝑆 )