Theorem elmgplsmd

Description: Membership in a product of two subsets of a multiplication group, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024)

	Ref	Expression
Hypotheses	elmgplsm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	elmgplsm.t	⊢ · = ( .r ‘ 𝑅 )
	elmgplsm.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	elmgplsm.m	⊢ × = ( LSSum ‘ 𝐺 )
	elmgplsm.e	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
	elmgplsm.f	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
	elmgplsmd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
	elmgplsmd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐹 )
Assertion	elmgplsmd	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ( 𝐸 × 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		elmgplsm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		elmgplsm.t	⊢ · = ( .r ‘ 𝑅 )
3		elmgplsm.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
4		elmgplsm.m	⊢ × = ( LSSum ‘ 𝐺 )
5		elmgplsm.e	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
6		elmgplsm.f	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
7		elmgplsmd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
8		elmgplsmd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐹 )
9		eqidd	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) )
10		rspceov	⊢ ( ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐹 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ( 𝑋 · 𝑌 ) = ( 𝑥 · 𝑦 ) )
11	7 8 9 10	syl3anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ( 𝑋 · 𝑌 ) = ( 𝑥 · 𝑦 ) )
12	1 2 3 4 5 6	elmgplsm	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ( 𝑋 · 𝑌 ) = ( 𝑥 · 𝑦 ) ) )
13	11 12	mpbird	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ( 𝐸 × 𝐹 ) )