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

Metamath Proof Explorer

Theorem dmmulsr

Description: Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion dmmulsr dom ·R = ( R × R )

Proof

Step Hyp Ref Expression
1 df-mr ⊢ ·R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑓 ) ) , ( ( 𝑤 ·P 𝑓 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) }
2 1 dmeqi ⊢ dom ·R = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑓 ) ) , ( ( 𝑤 ·P 𝑓 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) }
3 dmoprabss ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑓 ) ) , ( ( 𝑤 ·P 𝑓 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) } ⊆ ( R × R )
4 2 3 eqsstri ⊢ dom ·R ⊆ ( R × R )
5 0nsr ⊢ ¬ ∅ ∈ R
6 mulclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( 𝑥 ·R 𝑦 ) ∈ R )
7 5 6 oprssdm ⊢ ( R × R ) ⊆ dom ·R
8 4 7 eqssi ⊢ dom ·R = ( R × R )