Theorem elringlsm

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

	Ref	Expression
Hypotheses	elringlsm.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	elringlsm.2	⊢ · = ( .r ‘ 𝑅 )
	elringlsm.3	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	elringlsm.4	⊢ × = ( LSSum ‘ 𝐺 )
	elringlsm.6	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
	elringlsm.7	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
Assertion	elringlsm	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 𝑍 = ( 𝑥 · 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elringlsm.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		elringlsm.2	⊢ · = ( .r ‘ 𝑅 )
3		elringlsm.3	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
4		elringlsm.4	⊢ × = ( LSSum ‘ 𝐺 )
5		elringlsm.6	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
6		elringlsm.7	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
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	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 𝑍 = ( 𝑥 · 𝑦 ) ) )