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

Metamath Proof Explorer

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