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 )