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

Metamath Proof Explorer

Definition df-mul

Description: Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-mul · = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmul ⊢ ·
1 vx ⊢ 𝑥
2 vy ⊢ 𝑦
3 vz ⊢ 𝑧
4 1 cv ⊢ 𝑥
5 cc ⊢ ℂ
6 4 5 wcel ⊢ 𝑥 ∈ ℂ
7 2 cv ⊢ 𝑦
8 7 5 wcel ⊢ 𝑦 ∈ ℂ
9 6 8 wa ⊢ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ )
10 vw ⊢ 𝑤
11 vv ⊢ 𝑣
12 vu ⊢ 𝑢
13 vf ⊢ 𝑓
14 10 cv ⊢ 𝑤
15 11 cv ⊢ 𝑣
16 14 15 cop ⊢ ⟨ 𝑤 , 𝑣 ⟩
17 4 16 wceq ⊢ 𝑥 = ⟨ 𝑤 , 𝑣 ⟩
18 12 cv ⊢ 𝑢
19 13 cv ⊢ 𝑓
20 18 19 cop ⊢ ⟨ 𝑢 , 𝑓 ⟩
21 7 20 wceq ⊢ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩
22 17 21 wa ⊢ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ )
23 3 cv ⊢ 𝑧
24 cmr ⊢ ·R
25 14 18 24 co ⊢ ( 𝑤 ·R 𝑢 )
26 cplr ⊢ +R
27 cm1r ⊢ -1R
28 15 19 24 co ⊢ ( 𝑣 ·R 𝑓 )
29 27 28 24 co ⊢ ( -1R ·R ( 𝑣 ·R 𝑓 ) )
30 25 29 26 co ⊢ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) )
31 15 18 24 co ⊢ ( 𝑣 ·R 𝑢 )
32 14 19 24 co ⊢ ( 𝑤 ·R 𝑓 )
33 31 32 26 co ⊢ ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) )
34 30 33 cop ⊢ ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩
35 23 34 wceq ⊢ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩
36 22 35 wa ⊢ ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ )
37 36 13 wex ⊢ ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ )
38 37 12 wex ⊢ ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ )
39 38 11 wex ⊢ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ )
40 39 10 wex ⊢ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ )
41 9 40 wa ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) )
42 41 1 2 3 coprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }
43 0 42 wceq ⊢ · = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }