Step | Hyp | Ref
| Expression |
1 | | moeq 3606 |
. . . . . . . . 9
⊢
∃*𝑧 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉 |
2 | 1 | mosubop 5368 |
. . . . . . . 8
⊢
∃*𝑧∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉) |
3 | 2 | mosubop 5368 |
. . . . . . 7
⊢
∃*𝑧∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉)) |
4 | | anass 472 |
. . . . . . . . . . 11
⊢ (((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
5 | 4 | 2exbii 1855 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉) ↔ ∃𝑢∃𝑓(𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
6 | | 19.42vv 1965 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓(𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉)) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
7 | 5, 6 | bitri 278 |
. . . . . . . . 9
⊢
(∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
8 | 7 | 2exbii 1855 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉) ↔ ∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
9 | 8 | mobii 2548 |
. . . . . . 7
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉) ↔ ∃*𝑧∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
10 | 3, 9 | mpbir 234 |
. . . . . 6
⊢
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉) |
11 | 10 | moani 2553 |
. . . . 5
⊢
∃*𝑧((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉)) |
12 | 11 | funoprab 7290 |
. . . 4
⊢ Fun
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
13 | | df-mul 10629 |
. . . . 5
⊢ ·
= {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
14 | 13 | funeqi 6360 |
. . . 4
⊢ (Fun
· ↔ Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))}) |
15 | 12, 14 | mpbir 234 |
. . 3
⊢ Fun
· |
16 | 13 | dmeqi 5747 |
. . . . 5
⊢ dom
· = dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
17 | | dmoprabss 7272 |
. . . . 5
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} ⊆ (ℂ ×
ℂ) |
18 | 16, 17 | eqsstri 3911 |
. . . 4
⊢ dom
· ⊆ (ℂ × ℂ) |
19 | | 0ncn 10635 |
. . . . 5
⊢ ¬
∅ ∈ ℂ |
20 | | df-c 10623 |
. . . . . . 7
⊢ ℂ =
(R × R) |
21 | | oveq1 7179 |
. . . . . . . 8
⊢
(〈𝑧, 𝑤〉 = 𝑥 → (〈𝑧, 𝑤〉 · 〈𝑣, 𝑢〉) = (𝑥 · 〈𝑣, 𝑢〉)) |
22 | 21 | eleq1d 2817 |
. . . . . . 7
⊢
(〈𝑧, 𝑤〉 = 𝑥 → ((〈𝑧, 𝑤〉 · 〈𝑣, 𝑢〉) ∈ (R ×
R) ↔ (𝑥
· 〈𝑣, 𝑢〉) ∈ (R
× R))) |
23 | | oveq2 7180 |
. . . . . . . 8
⊢
(〈𝑣, 𝑢〉 = 𝑦 → (𝑥 · 〈𝑣, 𝑢〉) = (𝑥 · 𝑦)) |
24 | 23 | eleq1d 2817 |
. . . . . . 7
⊢
(〈𝑣, 𝑢〉 = 𝑦 → ((𝑥 · 〈𝑣, 𝑢〉) ∈ (R ×
R) ↔ (𝑥
· 𝑦) ∈
(R × R))) |
25 | | mulcnsr 10638 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (〈𝑧, 𝑤〉 · 〈𝑣, 𝑢〉) = 〈((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))), ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))〉) |
26 | | mulclsr 10586 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ R ∧
𝑣 ∈ R)
→ (𝑧
·R 𝑣) ∈ R) |
27 | | m1r 10584 |
. . . . . . . . . . . 12
⊢
-1R ∈ R |
28 | | mulclsr 10586 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (𝑤
·R 𝑢) ∈ R) |
29 | | mulclsr 10586 |
. . . . . . . . . . . 12
⊢
((-1R ∈ R ∧ (𝑤
·R 𝑢) ∈ R) →
(-1R ·R (𝑤
·R 𝑢)) ∈ R) |
30 | 27, 28, 29 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (-1R ·R (𝑤
·R 𝑢)) ∈ R) |
31 | | addclsr 10585 |
. . . . . . . . . . 11
⊢ (((𝑧
·R 𝑣) ∈ R ∧
(-1R ·R (𝑤
·R 𝑢)) ∈ R) → ((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
32 | 26, 30, 31 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ R ∧
𝑣 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
33 | 32 | an4s 660 |
. . . . . . . . 9
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
34 | | mulclsr 10586 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ R ∧
𝑣 ∈ R)
→ (𝑤
·R 𝑣) ∈ R) |
35 | | mulclsr 10586 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ R ∧
𝑢 ∈ R)
→ (𝑧
·R 𝑢) ∈ R) |
36 | | addclsr 10585 |
. . . . . . . . . . 11
⊢ (((𝑤
·R 𝑣) ∈ R ∧ (𝑧
·R 𝑢) ∈ R) → ((𝑤
·R 𝑣) +R (𝑧
·R 𝑢)) ∈ R) |
37 | 34, 35, 36 | syl2anr 600 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ R ∧
𝑢 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑣
∈ R)) → ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)) ∈ R) |
38 | 37 | an42s 661 |
. . . . . . . . 9
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)) ∈ R) |
39 | 33, 38 | opelxpd 5563 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → 〈((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))), ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))〉 ∈ (R ×
R)) |
40 | 25, 39 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (〈𝑧, 𝑤〉 · 〈𝑣, 𝑢〉) ∈ (R ×
R)) |
41 | 20, 22, 24, 40 | 2optocl 5617 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ (R ×
R)) |
42 | 41, 20 | eleqtrrdi 2844 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
43 | 19, 42 | oprssdm 7347 |
. . . 4
⊢ (ℂ
× ℂ) ⊆ dom · |
44 | 18, 43 | eqssi 3893 |
. . 3
⊢ dom
· = (ℂ × ℂ) |
45 | | df-fn 6342 |
. . 3
⊢ (
· Fn (ℂ × ℂ) ↔ (Fun · ∧ dom · =
(ℂ × ℂ))) |
46 | 15, 44, 45 | mpbir2an 711 |
. 2
⊢ ·
Fn (ℂ × ℂ) |
47 | 42 | rgen2 3115 |
. 2
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℂ (𝑥 · 𝑦) ∈
ℂ |
48 | | ffnov 7295 |
. 2
⊢ (
· :(ℂ × ℂ)⟶ℂ ↔ ( · Fn
(ℂ × ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (𝑥 · 𝑦) ∈ ℂ)) |
49 | 46, 47, 48 | mpbir2an 711 |
1
⊢ ·
:(ℂ × ℂ)⟶ℂ |