Definition df-mul 11184

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

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓

Detailed syntax breakdown of Definition df-mul

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

This definition is used by:  mulcnsr  11193  axmulf  11203