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

Metamath Proof Explorer

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 𝐷 ) ⟩ )