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

Metamath Proof Explorer

Theorem elringlsmd

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

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

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 elringlsmd.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
8 elringlsmd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐹 )
9 eqidd ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) )
10 rspceov ⊢ ( ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐹 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ( 𝑋 · 𝑌 ) = ( 𝑥 · 𝑦 ) )
11 7 8 9 10 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ( 𝑋 · 𝑌 ) = ( 𝑥 · 𝑦 ) )
12 1 2 3 4 5 6 elringlsm ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ∈ ( 𝐸 × 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐹 ( 𝑋 · 𝑌 ) = ( 𝑥 · 𝑦 ) ) )
13 11 12 mpbird ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ( 𝐸 × 𝐹 ) )