Metamath Proof Explorer

Theorem axaddf

Description: Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl . This construction-dependent theorem should not be referenced directly; instead, use ax-addf . (Contributed by NM, 8-Feb-2005) (New usage is discouraged.)

Ref Expression
Assertion axaddf + : ( ℂ × ℂ ) ⟶ ℂ

Proof

Step Hyp Ref Expression
1 moeq ⊢ ∃* 𝑧 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩
2 1 mosubop ⊢ ∃* 𝑧 ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ )
3 2 mosubop ⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) )
4 anass ⊢ ( ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) )
5 4 2exbii ⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ↔ ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) )
6 19.42vv ⊢ ( ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) )
7 5 6 bitri ⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) )
8 7 2exbii ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ↔ ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) )
9 8 mobii ⊢ ( ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ↔ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) )
10 3 9 mpbir ⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ )
11 10 moani ⊢ ∃* 𝑧 ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) )
12 11 funoprab ⊢ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) }
13 df-add ⊢ + = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) }
14 13 funeqi ⊢ ( Fun + ↔ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) } )
15 12 14 mpbir ⊢ Fun +
16 13 dmeqi ⊢ dom + = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) }
17 dmoprabss ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) } ⊆ ( ℂ × ℂ )
18 16 17 eqsstri ⊢ dom + ⊆ ( ℂ × ℂ )
19 0ncn ⊢ ¬ ∅ ∈ ℂ
20 df-c ⊢ ℂ = ( R × R )
21 oveq1 ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = 𝑥 → ( ⟨ 𝑧 , 𝑤 ⟩ + ⟨ 𝑣 , 𝑢 ⟩ ) = ( 𝑥 + ⟨ 𝑣 , 𝑢 ⟩ ) )
22 21 eleq1d ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = 𝑥 → ( ( ⟨ 𝑧 , 𝑤 ⟩ + ⟨ 𝑣 , 𝑢 ⟩ ) ∈ ( R × R ) ↔ ( 𝑥 + ⟨ 𝑣 , 𝑢 ⟩ ) ∈ ( R × R ) ) )
23 oveq2 ⊢ ( ⟨ 𝑣 , 𝑢 ⟩ = 𝑦 → ( 𝑥 + ⟨ 𝑣 , 𝑢 ⟩ ) = ( 𝑥 + 𝑦 ) )
24 23 eleq1d ⊢ ( ⟨ 𝑣 , 𝑢 ⟩ = 𝑦 → ( ( 𝑥 + ⟨ 𝑣 , 𝑢 ⟩ ) ∈ ( R × R ) ↔ ( 𝑥 + 𝑦 ) ∈ ( R × R ) ) )
25 addcnsr ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ + ⟨ 𝑣 , 𝑢 ⟩ ) = ⟨ ( 𝑧 +R 𝑣 ) , ( 𝑤 +R 𝑢 ) ⟩ )
26 addclsr ⊢ ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑧 +R 𝑣 ) ∈ R )
27 addclsr ⊢ ( ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑤 +R 𝑢 ) ∈ R )
28 26 27 anim12i ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) ∧ ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) )
29 28 an4s ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) )
30 opelxpi ⊢ ( ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) → ⟨ ( 𝑧 +R 𝑣 ) , ( 𝑤 +R 𝑢 ) ⟩ ∈ ( R × R ) )
31 29 30 syl ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ⟨ ( 𝑧 +R 𝑣 ) , ( 𝑤 +R 𝑢 ) ⟩ ∈ ( R × R ) )
32 25 31 eqeltrd ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ + ⟨ 𝑣 , 𝑢 ⟩ ) ∈ ( R × R ) )
33 20 22 24 32 2optocl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ( R × R ) )
34 33 20 eleqtrrdi ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
35 19 34 oprssdm ⊢ ( ℂ × ℂ ) ⊆ dom +
36 18 35 eqssi ⊢ dom + = ( ℂ × ℂ )
37 df-fn ⊢ ( + Fn ( ℂ × ℂ ) ↔ ( Fun + ∧ dom + = ( ℂ × ℂ ) ) )
38 15 36 37 mpbir2an ⊢ + Fn ( ℂ × ℂ )
39 34 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) ∈ ℂ
40 ffnov ⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ ↔ ( + Fn ( ℂ × ℂ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) ∈ ℂ ) )
41 38 39 40 mpbir2an ⊢ + : ( ℂ × ℂ ) ⟶ ℂ