Metamath Proof Explorer

Theorem axmulf

Description: Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl . (Contributed by NM, 8-Feb-2005) (New usage is discouraged.)

Ref Expression
Assertion axmulf · : ( ℂ × ℂ ) ⟶ ℂ

Proof

Step Hyp Ref Expression
1 moeq ⊢ ∃* 𝑧 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩
2 1 mosubop ⊢ ∃* 𝑧 ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ )
3 2 mosubop ⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) )
4 anass ⊢ ( ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) )
5 4 2exbii ⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ↔ ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) )
6 19.42vv ⊢ ( ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) )
7 5 6 bitri ⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) )
8 7 2exbii ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ↔ ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) )
9 8 mobii ⊢ ( ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ↔ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) )
10 3 9 mpbir ⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ )
11 10 moani ⊢ ∃* 𝑧 ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) )
12 11 funoprab ⊢ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }
13 df-mul ⊢ · = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }
14 13 funeqi ⊢ ( Fun · ↔ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) } )
15 12 14 mpbir ⊢ Fun ·
16 13 dmeqi ⊢ dom · = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }
17 dmoprabss ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +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 mulcnsr ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ · ⟨ 𝑣 , 𝑢 ⟩ ) = ⟨ ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) , ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ⟩ )
26 mulclsr ⊢ ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑧 ·R 𝑣 ) ∈ R )
27 m1r ⊢ -1R ∈ R
28 mulclsr ⊢ ( ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑤 ·R 𝑢 ) ∈ R )
29 mulclsr ⊢ ( ( -1R ∈ R ∧ ( 𝑤 ·R 𝑢 ) ∈ R ) → ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ∈ R )
30 27 28 29 sylancr ⊢ ( ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) → ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ∈ R )
31 addclsr ⊢ ( ( ( 𝑧 ·R 𝑣 ) ∈ R ∧ ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ∈ R ) → ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R )
32 26 30 31 syl2an ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) ∧ ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R )
33 32 an4s ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R )
34 mulclsr ⊢ ( ( 𝑤 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑤 ·R 𝑣 ) ∈ R )
35 mulclsr ⊢ ( ( 𝑧 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑧 ·R 𝑢 ) ∈ R )
36 addclsr ⊢ ( ( ( 𝑤 ·R 𝑣 ) ∈ R ∧ ( 𝑧 ·R 𝑢 ) ∈ R ) → ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R )
37 34 35 36 syl2anr ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑢 ∈ R ) ∧ ( 𝑤 ∈ R ∧ 𝑣 ∈ R ) ) → ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R )
38 37 an42s ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R )
39 33 38 opelxpd ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ⟨ ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) , ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ⟩ ∈ ( R × R ) )
40 25 39 eqeltrd ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ · ⟨ 𝑣 , 𝑢 ⟩ ) ∈ ( R × R ) )
41 20 22 24 40 2optocl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ( R × R ) )
42 41 20 eleqtrrdi ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
43 19 42 oprssdm ⊢ ( ℂ × ℂ ) ⊆ dom ·
44 18 43 eqssi ⊢ dom · = ( ℂ × ℂ )
45 df-fn ⊢ ( · Fn ( ℂ × ℂ ) ↔ ( Fun · ∧ dom · = ( ℂ × ℂ ) ) )
46 15 44 45 mpbir2an ⊢ · Fn ( ℂ × ℂ )
47 42 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑥 · 𝑦 ) ∈ ℂ
48 ffnov ⊢ ( · : ( ℂ × ℂ ) ⟶ ℂ ↔ ( · Fn ( ℂ × ℂ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑥 · 𝑦 ) ∈ ℂ ) )
49 46 47 48 mpbir2an ⊢ · : ( ℂ × ℂ ) ⟶ ℂ