Step | Hyp | Ref
| Expression |
1 | | opex 5426 |
. 2
⊢
⟨(𝐴
+R 𝐶), (𝐵 +R 𝐷)⟩ ∈
V |
2 | | oveq1 7369 |
. . . 4
⊢ (𝑤 = 𝐴 → (𝑤 +R 𝑢) = (𝐴 +R 𝑢)) |
3 | | oveq1 7369 |
. . . 4
⊢ (𝑣 = 𝐵 → (𝑣 +R 𝑓) = (𝐵 +R 𝑓)) |
4 | | opeq12 4837 |
. . . 4
⊢ (((𝑤 +R
𝑢) = (𝐴 +R 𝑢) ∧ (𝑣 +R 𝑓) = (𝐵 +R 𝑓)) → ⟨(𝑤 +R
𝑢), (𝑣 +R 𝑓)⟩ = ⟨(𝐴 +R
𝑢), (𝐵 +R 𝑓)⟩) |
5 | 2, 3, 4 | syl2an 597 |
. . 3
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩ = ⟨(𝐴 +R
𝑢), (𝐵 +R 𝑓)⟩) |
6 | | oveq2 7370 |
. . . 4
⊢ (𝑢 = 𝐶 → (𝐴 +R 𝑢) = (𝐴 +R 𝐶)) |
7 | | oveq2 7370 |
. . . 4
⊢ (𝑓 = 𝐷 → (𝐵 +R 𝑓) = (𝐵 +R 𝐷)) |
8 | | opeq12 4837 |
. . . 4
⊢ (((𝐴 +R
𝑢) = (𝐴 +R 𝐶) ∧ (𝐵 +R 𝑓) = (𝐵 +R 𝐷)) → ⟨(𝐴 +R
𝑢), (𝐵 +R 𝑓)⟩ = ⟨(𝐴 +R
𝐶), (𝐵 +R 𝐷)⟩) |
9 | 6, 7, 8 | syl2an 597 |
. . 3
⊢ ((𝑢 = 𝐶 ∧ 𝑓 = 𝐷) → ⟨(𝐴 +R 𝑢), (𝐵 +R 𝑓)⟩ = ⟨(𝐴 +R
𝐶), (𝐵 +R 𝐷)⟩) |
10 | 5, 9 | sylan9eq 2797 |
. 2
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩ = ⟨(𝐴 +R
𝐶), (𝐵 +R 𝐷)⟩) |
11 | | df-add 11069 |
. . 3
⊢ + =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} |
12 | | df-c 11064 |
. . . . . . 7
⊢ ℂ =
(R × R) |
13 | 12 | eleq2i 2830 |
. . . . . 6
⊢ (𝑥 ∈ ℂ ↔ 𝑥 ∈ (R ×
R)) |
14 | 12 | eleq2i 2830 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↔ 𝑦 ∈ (R ×
R)) |
15 | 13, 14 | anbi12i 628 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ↔ (𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R))) |
16 | 15 | anbi1i 625 |
. . . 4
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩)) ↔ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))) |
17 | 16 | oprabbii 7429 |
. . 3
⊢
{⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} |
18 | 11, 17 | eqtri 2765 |
. 2
⊢ + =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} |
19 | 1, 10, 18 | ov3 7522 |
1
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩) |