Theorem dmaddsr

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

	Ref	Expression
Assertion	dmaddsr	⊢ dom +R = ( R × R )

Proof

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