Step | Hyp | Ref
| Expression |
1 | | mulclsr 7677 |
. . . . 5
⊢ ((𝐴 ∈ R ∧
𝐶 ∈ R)
→ (𝐴
·R 𝐶) ∈ R) |
2 | 1 | ad2ant2r 501 |
. . . 4
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (𝐴 ·R 𝐶) ∈
R) |
3 | | m1r 7675 |
. . . . 5
⊢
-1R ∈ R |
4 | | mulclsr 7677 |
. . . . . 6
⊢ ((𝐵 ∈ R ∧
𝐷 ∈ R)
→ (𝐵
·R 𝐷) ∈ R) |
5 | 4 | ad2ant2l 500 |
. . . . 5
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (𝐵 ·R 𝐷) ∈
R) |
6 | | mulclsr 7677 |
. . . . 5
⊢
((-1R ∈ R ∧ (𝐵
·R 𝐷) ∈ R) →
(-1R ·R (𝐵
·R 𝐷)) ∈ R) |
7 | 3, 5, 6 | sylancr 411 |
. . . 4
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (-1R
·R (𝐵 ·R 𝐷)) ∈
R) |
8 | | addclsr 7676 |
. . . 4
⊢ (((𝐴
·R 𝐶) ∈ R ∧
(-1R ·R (𝐵
·R 𝐷)) ∈ R) → ((𝐴
·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))) ∈ R) |
9 | 2, 7, 8 | syl2anc 409 |
. . 3
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → ((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))) ∈ R) |
10 | | mulclsr 7677 |
. . . . 5
⊢ ((𝐵 ∈ R ∧
𝐶 ∈ R)
→ (𝐵
·R 𝐶) ∈ R) |
11 | 10 | ad2ant2lr 502 |
. . . 4
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (𝐵 ·R 𝐶) ∈
R) |
12 | | mulclsr 7677 |
. . . . 5
⊢ ((𝐴 ∈ R ∧
𝐷 ∈ R)
→ (𝐴
·R 𝐷) ∈ R) |
13 | 12 | ad2ant2rl 503 |
. . . 4
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (𝐴 ·R 𝐷) ∈
R) |
14 | | addclsr 7676 |
. . . 4
⊢ (((𝐵
·R 𝐶) ∈ R ∧ (𝐴
·R 𝐷) ∈ R) → ((𝐵
·R 𝐶) +R (𝐴
·R 𝐷)) ∈ R) |
15 | 11, 13, 14 | syl2anc 409 |
. . 3
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷)) ∈ R) |
16 | | opelxpi 4621 |
. . 3
⊢ ((((𝐴
·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))) ∈ R ∧ ((𝐵
·R 𝐶) +R (𝐴
·R 𝐷)) ∈ R) →
〈((𝐴
·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉 ∈ (R ×
R)) |
17 | 9, 15, 16 | syl2anc 409 |
. 2
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → 〈((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉 ∈ (R ×
R)) |
18 | | simpll 519 |
. . . . 5
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑤 = 𝐴) |
19 | | simprl 521 |
. . . . 5
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑢 = 𝐶) |
20 | 18, 19 | oveq12d 5845 |
. . . 4
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → (𝑤 ·R 𝑢) = (𝐴 ·R 𝐶)) |
21 | | simplr 520 |
. . . . . 6
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑣 = 𝐵) |
22 | | simprr 522 |
. . . . . 6
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑓 = 𝐷) |
23 | 21, 22 | oveq12d 5845 |
. . . . 5
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → (𝑣 ·R 𝑓) = (𝐵 ·R 𝐷)) |
24 | 23 | oveq2d 5843 |
. . . 4
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → (-1R
·R (𝑣 ·R 𝑓)) =
(-1R ·R (𝐵
·R 𝐷))) |
25 | 20, 24 | oveq12d 5845 |
. . 3
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → ((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))) = ((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷)))) |
26 | 21, 19 | oveq12d 5845 |
. . . 4
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → (𝑣 ·R 𝑢) = (𝐵 ·R 𝐶)) |
27 | 18, 22 | oveq12d 5845 |
. . . 4
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → (𝑤 ·R 𝑓) = (𝐴 ·R 𝐷)) |
28 | 26, 27 | oveq12d 5845 |
. . 3
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓)) = ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))) |
29 | 25, 28 | opeq12d 3751 |
. 2
⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉 = 〈((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉) |
30 | | df-mul 7747 |
. . 3
⊢ ·
= {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
31 | | df-c 7741 |
. . . . . . 7
⊢ ℂ =
(R × R) |
32 | 31 | eleq2i 2224 |
. . . . . 6
⊢ (𝑥 ∈ ℂ ↔ 𝑥 ∈ (R ×
R)) |
33 | 31 | eleq2i 2224 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↔ 𝑦 ∈ (R ×
R)) |
34 | 32, 33 | anbi12i 456 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ↔ (𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R))) |
35 | 34 | anbi1i 454 |
. . . 4
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉)) ↔ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))) |
36 | 35 | oprabbii 5879 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
37 | 30, 36 | eqtri 2178 |
. 2
⊢ ·
= {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (R ×
R) ∧ 𝑦
∈ (R × R)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))〉))} |
38 | 17, 29, 37 | ovi3 5960 |
1
⊢ (((𝐴 ∈ R ∧
𝐵 ∈ R)
∧ (𝐶 ∈
R ∧ 𝐷
∈ R)) → (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) = 〈((𝐴 ·R 𝐶) +R
(-1R ·R (𝐵
·R 𝐷))), ((𝐵 ·R 𝐶) +R
(𝐴
·R 𝐷))〉) |