Theorem addcnsr

Description: Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	addcnsr	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ + ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ ∈ V
2		oveq1	⊢ ( 𝑤 = 𝐴 → ( 𝑤 +R 𝑢 ) = ( 𝐴 +R 𝑢 ) )
3		oveq1	⊢ ( 𝑣 = 𝐵 → ( 𝑣 +R 𝑓 ) = ( 𝐵 +R 𝑓 ) )
4		opeq12	⊢ ( ( ( 𝑤 +R 𝑢 ) = ( 𝐴 +R 𝑢 ) ∧ ( 𝑣 +R 𝑓 ) = ( 𝐵 +R 𝑓 ) ) → ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ = ⟨ ( 𝐴 +R 𝑢 ) , ( 𝐵 +R 𝑓 ) ⟩ )
5	2 3 4	syl2an	⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ = ⟨ ( 𝐴 +R 𝑢 ) , ( 𝐵 +R 𝑓 ) ⟩ )
6		oveq2	⊢ ( 𝑢 = 𝐶 → ( 𝐴 +R 𝑢 ) = ( 𝐴 +R 𝐶 ) )
7		oveq2	⊢ ( 𝑓 = 𝐷 → ( 𝐵 +R 𝑓 ) = ( 𝐵 +R 𝐷 ) )
8		opeq12	⊢ ( ( ( 𝐴 +R 𝑢 ) = ( 𝐴 +R 𝐶 ) ∧ ( 𝐵 +R 𝑓 ) = ( 𝐵 +R 𝐷 ) ) → ⟨ ( 𝐴 +R 𝑢 ) , ( 𝐵 +R 𝑓 ) ⟩ = ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ )
9	6 7 8	syl2an	⊢ ( ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) → ⟨ ( 𝐴 +R 𝑢 ) , ( 𝐵 +R 𝑓 ) ⟩ = ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ )
10	5 9	sylan9eq	⊢ ( ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) ∧ ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) ) → ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ = ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ )
11		df-add	⊢ + = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) }
12		df-c	⊢ ℂ = ( R × R )
13	12	eleq2i	⊢ ( 𝑥 ∈ ℂ ↔ 𝑥 ∈ ( R × R ) )
14	12	eleq2i	⊢ ( 𝑦 ∈ ℂ ↔ 𝑦 ∈ ( R × R ) )
15	13 14	anbi12i	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ↔ ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) )
16	15	anbi1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) ↔ ( ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) )
17	16	oprabbii	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) }
18	11 17	eqtri	⊢ + = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) }
19	1 10 18	ov3	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ + ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ )