Step | Hyp | Ref
| Expression |
1 | | moeq 3670 |
. . . . . . . . 9
⊢
∃*𝑧 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩ |
2 | 1 | mosubop 5473 |
. . . . . . . 8
⊢
∃*𝑧∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩) |
3 | 2 | mosubop 5473 |
. . . . . . 7
⊢
∃*𝑧∃𝑤∃𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩)) |
4 | | anass 470 |
. . . . . . . . . . 11
⊢ (((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))) |
5 | 4 | 2exbii 1852 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩) ↔ ∃𝑢∃𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))) |
6 | | 19.42vv 1962 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩)) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))) |
7 | 5, 6 | bitri 275 |
. . . . . . . . 9
⊢
(∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))) |
8 | 7 | 2exbii 1852 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩) ↔ ∃𝑤∃𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))) |
9 | 8 | mobii 2547 |
. . . . . . 7
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩) ↔ ∃*𝑧∃𝑤∃𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))) |
10 | 3, 9 | mpbir 230 |
. . . . . 6
⊢
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩) |
11 | 10 | moani 2552 |
. . . . 5
⊢
∃*𝑧((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩)) |
12 | 11 | funoprab 7483 |
. . . 4
⊢ Fun
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))} |
13 | | df-mul 11070 |
. . . . 5
⊢ ·
= {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))} |
14 | 13 | funeqi 6527 |
. . . 4
⊢ (Fun
· ↔ Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))}) |
15 | 12, 14 | mpbir 230 |
. . 3
⊢ Fun
· |
16 | 13 | dmeqi 5865 |
. . . . 5
⊢ dom
· = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))} |
17 | | dmoprabss 7464 |
. . . . 5
⊢ dom
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))} ⊆ (ℂ ×
ℂ) |
18 | 16, 17 | eqsstri 3983 |
. . . 4
⊢ dom
· ⊆ (ℂ × ℂ) |
19 | | 0ncn 11076 |
. . . . 5
⊢ ¬
∅ ∈ ℂ |
20 | | df-c 11064 |
. . . . . . 7
⊢ ℂ =
(R × R) |
21 | | oveq1 7369 |
. . . . . . . 8
⊢
(⟨𝑧, 𝑤⟩ = 𝑥 → (⟨𝑧, 𝑤⟩ · ⟨𝑣, 𝑢⟩) = (𝑥 · ⟨𝑣, 𝑢⟩)) |
22 | 21 | eleq1d 2823 |
. . . . . . 7
⊢
(⟨𝑧, 𝑤⟩ = 𝑥 → ((⟨𝑧, 𝑤⟩ · ⟨𝑣, 𝑢⟩) ∈ (R ×
R) ↔ (𝑥
· ⟨𝑣, 𝑢⟩) ∈ (R
× R))) |
23 | | oveq2 7370 |
. . . . . . . 8
⊢
(⟨𝑣, 𝑢⟩ = 𝑦 → (𝑥 · ⟨𝑣, 𝑢⟩) = (𝑥 · 𝑦)) |
24 | 23 | eleq1d 2823 |
. . . . . . 7
⊢
(⟨𝑣, 𝑢⟩ = 𝑦 → ((𝑥 · ⟨𝑣, 𝑢⟩) ∈ (R ×
R) ↔ (𝑥
· 𝑦) ∈
(R × R))) |
25 | | mulcnsr 11079 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (⟨𝑧, 𝑤⟩ · ⟨𝑣, 𝑢⟩) = ⟨((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))), ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))⟩) |
26 | | mulclsr 11027 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ R ∧
𝑣 ∈ R)
→ (𝑧
·R 𝑣) ∈ R) |
27 | | m1r 11025 |
. . . . . . . . . . . 12
⊢
-1R ∈ R |
28 | | mulclsr 11027 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (𝑤
·R 𝑢) ∈ R) |
29 | | mulclsr 11027 |
. . . . . . . . . . . 12
⊢
((-1R ∈ R ∧ (𝑤
·R 𝑢) ∈ R) →
(-1R ·R (𝑤
·R 𝑢)) ∈ R) |
30 | 27, 28, 29 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (-1R ·R (𝑤
·R 𝑢)) ∈ R) |
31 | | addclsr 11026 |
. . . . . . . . . . 11
⊢ (((𝑧
·R 𝑣) ∈ R ∧
(-1R ·R (𝑤
·R 𝑢)) ∈ R) → ((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
32 | 26, 30, 31 | syl2an 597 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ R ∧
𝑣 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
33 | 32 | an4s 659 |
. . . . . . . . 9
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
34 | | mulclsr 11027 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ R ∧
𝑣 ∈ R)
→ (𝑤
·R 𝑣) ∈ R) |
35 | | mulclsr 11027 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ R ∧
𝑢 ∈ R)
→ (𝑧
·R 𝑢) ∈ R) |
36 | | addclsr 11026 |
. . . . . . . . . . 11
⊢ (((𝑤
·R 𝑣) ∈ R ∧ (𝑧
·R 𝑢) ∈ R) → ((𝑤
·R 𝑣) +R (𝑧
·R 𝑢)) ∈ R) |
37 | 34, 35, 36 | syl2anr 598 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ R ∧
𝑢 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑣
∈ R)) → ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)) ∈ R) |
38 | 37 | an42s 660 |
. . . . . . . . 9
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)) ∈ R) |
39 | 33, 38 | opelxpd 5676 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ⟨((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))), ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))⟩ ∈ (R ×
R)) |
40 | 25, 39 | eqeltrd 2838 |
. . . . . . 7
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (⟨𝑧, 𝑤⟩ · ⟨𝑣, 𝑢⟩) ∈ (R ×
R)) |
41 | 20, 22, 24, 40 | 2optocl 5732 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ (R ×
R)) |
42 | 41, 20 | eleqtrrdi 2849 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
43 | 19, 42 | oprssdm 7540 |
. . . 4
⊢ (ℂ
× ℂ) ⊆ dom · |
44 | 18, 43 | eqssi 3965 |
. . 3
⊢ dom
· = (ℂ × ℂ) |
45 | | df-fn 6504 |
. . 3
⊢ (
· Fn (ℂ × ℂ) ↔ (Fun · ∧ dom · =
(ℂ × ℂ))) |
46 | 15, 44, 45 | mpbir2an 710 |
. 2
⊢ ·
Fn (ℂ × ℂ) |
47 | 42 | rgen2 3195 |
. 2
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℂ (𝑥 · 𝑦) ∈
ℂ |
48 | | ffnov 7488 |
. 2
⊢ (
· :(ℂ × ℂ)⟶ℂ ↔ ( · Fn
(ℂ × ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (𝑥 · 𝑦) ∈ ℂ)) |
49 | 46, 47, 48 | mpbir2an 710 |
1
⊢ ·
:(ℂ × ℂ)⟶ℂ |