This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 𝑍 = ( 𝑥 · 𝑦 ) ) )