Theorem elmgplsm

Description: Membership in a product of two subsets of a multiplication group. (Contributed by Thierry Arnoux, 20-Jan-2024)

	Ref	Expression
Hypotheses	elmgplsm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	elmgplsm.t	⊢ · = ( .r ‘ 𝑅 )
	elmgplsm.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	elmgplsm.m	⊢ × = ( LSSum ‘ 𝐺 )
	elmgplsm.e	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
	elmgplsm.f	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
Assertion	elmgplsm	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 𝑍 = ( 𝑥 · 𝑦 ) ) )

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	3	fvexi	⊢ 𝐺 ∈ V
8	3 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝐺 )
9	3 2	mgpplusg	⊢ · = ( +g ‘ 𝐺 )
10	8 9 4	lsmelvalx	⊢ ( ( 𝐺 ∈ V ∧ 𝐸 ⊆ 𝐵 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝑍 ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 𝑍 = ( 𝑥 · 𝑦 ) ) )
11	7 5 6 10	mp3an2i	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 𝑍 = ( 𝑥 · 𝑦 ) ) )