Definition df-mul 4040

Description: Define multiplication over complex numbers.

Assertion

Ref	Expression
df-mul	⊢ · = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩))}

Distinct variable group(s):   x,y,z,w,v,u,f

Detailed syntax breakdown of Definition df-mul

Step	Hyp	Ref	Expression
1		cmulc 4032	. 2 class ·
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cc 4026	. . . . . 6 class ℂ
5	3, 4	wcel 1092	. . . . 5 wff x ∈ ℂ
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ ℂ
9	5, 8	wa 196	. . . 4 wff (x ∈ ℂ ∧ y ∈ ℂ)
10		vw	. . . . . . . . . . . . 13 set w
11	10	cv 1089	. . . . . . . . . . . 12 class w
12		vv	. . . . . . . . . . . . 13 set v
13	12	cv 1089	. . . . . . . . . . . 12 class v
14	11, 13	cop 1810	. . . . . . . . . . 11 class ⟨w, v⟩
15	3, 14	wceq 1091	. . . . . . . . . 10 wff x = ⟨w, v⟩
16		vu	. . . . . . . . . . . . 13 set u
17	16	cv 1089	. . . . . . . . . . . 12 class u
18		vf	. . . . . . . . . . . . 13 set f
19	18	cv 1089	. . . . . . . . . . . 12 class f
20	17, 19	cop 1810	. . . . . . . . . . 11 class ⟨u, f⟩
21	7, 20	wceq 1091	. . . . . . . . . 10 wff y = ⟨u, f⟩
22	15, 21	wa 196	. . . . . . . . 9 wff (x = ⟨w, v⟩ ∧ y = ⟨u, f⟩)
23		vz	. . . . . . . . . . 11 set z
24	23	cv 1089	. . . . . . . . . 10 class z
25		cmr 3792	. . . . . . . . . . . . 13 class ·R
26	11, 17, 25	co 3001	. . . . . . . . . . . 12 class (w ·R u)
27		cm1r 3790	. . . . . . . . . . . . 13 class -1R
28	13, 19, 25	co 3001	. . . . . . . . . . . . 13 class (v ·R f)
29	27, 28, 25	co 3001	. . . . . . . . . . . 12 class (-1R ·R (v ·R f))
30		cplr 3791	. . . . . . . . . . . 12 class +R
31	26, 29, 30	co 3001	. . . . . . . . . . 11 class ((w ·R u) +R (-1R ·R (v ·R f)))
32	13, 17, 25	co 3001	. . . . . . . . . . . 12 class (v ·R u)
33	11, 19, 25	co 3001	. . . . . . . . . . . 12 class (w ·R f)
34	32, 33, 30	co 3001	. . . . . . . . . . 11 class ((v ·R u) +R (w ·R f))
35	31, 34	cop 1810	. . . . . . . . . 10 class ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩
36	24, 35	wceq 1091	. . . . . . . . 9 wff z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩
37	22, 36	wa 196	. . . . . . . 8 wff ((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩)
38	37, 18	wex 678	. . . . . . 7 wff ∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩)
39	38, 16	wex 678	. . . . . 6 wff ∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩)
40	39, 12	wex 678	. . . . 5 wff ∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩)
41	40, 10	wex 678	. . . 4 wff ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩)
42	9, 41	wa 196	. . 3 wff ((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩))
43	42, 2, 6, 23	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩))}
44	1, 43	wceq 1091	1 wff · = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩))}

This definition is referenced by:  mulcnsr 4048  axmulex 4060

metamath.org