Step | Hyp | Ref
| Expression |
1 | | opex 5379 |
. 2
⊢
〈((𝐴
·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉 ∈ V |
2 | | oveq1 7282 |
. . . . 5
⊢ (𝑤 = 𝐴 → (𝑤 ·R 𝑢) = (𝐴 ·R 𝑢)) |
3 | | oveq1 7282 |
. . . . . 6
⊢ (𝑣 = 𝐵 → (𝑣 ·R 𝑓) = (𝐵 ·R 𝑓)) |
4 | 3 | oveq2d 7291 |
. . . . 5
⊢ (𝑣 = 𝐵 → (-1R
·R (𝑣 ·R 𝑓)) =
(-1R ·R (𝐵
·R 𝑓))) |
5 | 2, 4 | oveqan12d 7294 |
. . . 4
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))) = ((𝐴 ·R 𝑢) +R
(-1R ·R (𝐵
·R 𝑓)))) |
6 | | oveq1 7282 |
. . . . 5
⊢ (𝑣 = 𝐵 → (𝑣 ·R 𝑢) = (𝐵 ·R 𝑢)) |
7 | | oveq1 7282 |
. . . . 5
⊢ (𝑤 = 𝐴 → (𝑤 ·R 𝑓) = (𝐴 ·R 𝑓)) |
8 | 6, 7 | oveqan12rd 7295 |
. . . 4
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓)) = ((𝐵 ·R 𝑢) +R
(𝐴
·R 𝑓))) |
9 | 5, 8 | opeq12d 4812 |
. . 3
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉 = 〈((𝐴 ·R 𝑢) +R
(-1R ·R (𝐵
·R 𝑓))), ((𝐵 ·R 𝑢) +R
(𝐴
·R 𝑓))〉) |
10 | | oveq2 7283 |
. . . . 5
⊢ (𝑢 = 𝐶 → (𝐴 ·R 𝑢) = (𝐴 ·R 𝐶)) |
11 | | oveq2 7283 |
. . . . . 6
⊢ (𝑓 = 𝐷 → (𝐵 ·R 𝑓) = (𝐵 ·R 𝐷)) |
12 | 11 | oveq2d 7291 |
. . . . 5
⊢ (𝑓 = 𝐷 → (-1R
·R (𝐵 ·R 𝑓)) =
(-1R ·R (𝐵
·R 𝐷))) |
13 | 10, 12 | oveqan12d 7294 |
. . . 4
⊢ ((𝑢 = 𝐶 ∧ 𝑓 = 𝐷) → ((𝐴 ·R 𝑢) +R
(-1R ·R (𝐵
·R 𝑓))) = ((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷)))) |
14 | | oveq2 7283 |
. . . . 5
⊢ (𝑢 = 𝐶 → (𝐵 ·R 𝑢) = (𝐵 ·R 𝐶)) |
15 | | oveq2 7283 |
. . . . 5
⊢ (𝑓 = 𝐷 → (𝐴 ·R 𝑓) = (𝐴 ·R 𝐷)) |
16 | 14, 15 | oveqan12d 7294 |
. . . 4
⊢ ((𝑢 = 𝐶 ∧ 𝑓 = 𝐷) → ((𝐵 ·R 𝑢) +R
(𝐴
·R 𝑓)) = ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))) |
17 | 13, 16 | opeq12d 4812 |
. . 3
⊢ ((𝑢 = 𝐶 ∧ 𝑓 = 𝐷) → 〈((𝐴 ·R 𝑢) +R
(-1R ·R (𝐵
·R 𝑓))), ((𝐵 ·R 𝑢) +R
(𝐴
·R 𝑓))〉 = 〈((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉) |
18 | 9, 17 | sylan9eq 2798 |
. 2
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉 = 〈((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉) |
19 | | df-mul 10883 |
. . 3
⊢ ·
= {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
20 | | df-c 10877 |
. . . . . . 7
⊢ ℂ =
(R × R) |
21 | 20 | eleq2i 2830 |
. . . . . 6
⊢ (𝑥 ∈ ℂ ↔ 𝑥 ∈ (R ×
R)) |
22 | 20 | eleq2i 2830 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↔ 𝑦 ∈ (R ×
R)) |
23 | 21, 22 | anbi12i 627 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ↔ (𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R))) |
24 | 23 | anbi1i 624 |
. . . 4
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉)) ↔ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
25 | 24 | oprabbii 7342 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
26 | 19, 25 | eqtri 2766 |
. 2
⊢ ·
= {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
27 | 1, 18, 26 | ov3 7435 |
1
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) = 〈((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉) |