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 𝑓 ) ) ⟩ ) ) }