Definition df-mr

Description: Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mr	⊢ ·R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑓 ) ) , ( ( 𝑤 ·P 𝑓 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) }

Detailed syntax breakdown

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