Step | Hyp | Ref
| Expression |
1 | | oveq12 5521 |
. 2
⊢ (((𝐴
·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → ((𝐴 ·N 𝐷)
·N (𝐹 ·N 𝑆)) = ((𝐵 ·N 𝐶)
·N (𝐺 ·N 𝑅))) |
2 | | mulclpi 6426 |
. . . . . . . 8
⊢ ((𝐴 ∈ N ∧
𝐹 ∈ N)
→ (𝐴
·N 𝐹) ∈ N) |
3 | | mulclpi 6426 |
. . . . . . . 8
⊢ ((𝐵 ∈ N ∧
𝐺 ∈ N)
→ (𝐵
·N 𝐺) ∈ N) |
4 | 2, 3 | anim12i 321 |
. . . . . . 7
⊢ (((𝐴 ∈ N ∧
𝐹 ∈ N)
∧ (𝐵 ∈
N ∧ 𝐺
∈ N)) → ((𝐴 ·N 𝐹) ∈ N ∧
(𝐵
·N 𝐺) ∈ N)) |
5 | 4 | an4s 522 |
. . . . . 6
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐹 ∈
N ∧ 𝐺
∈ N)) → ((𝐴 ·N 𝐹) ∈ N ∧
(𝐵
·N 𝐺) ∈ N)) |
6 | | mulclpi 6426 |
. . . . . . . 8
⊢ ((𝐶 ∈ N ∧
𝑅 ∈ N)
→ (𝐶
·N 𝑅) ∈ N) |
7 | | mulclpi 6426 |
. . . . . . . 8
⊢ ((𝐷 ∈ N ∧
𝑆 ∈ N)
→ (𝐷
·N 𝑆) ∈ N) |
8 | 6, 7 | anim12i 321 |
. . . . . . 7
⊢ (((𝐶 ∈ N ∧
𝑅 ∈ N)
∧ (𝐷 ∈
N ∧ 𝑆
∈ N)) → ((𝐶 ·N 𝑅) ∈ N ∧
(𝐷
·N 𝑆) ∈ N)) |
9 | 8 | an4s 522 |
. . . . . 6
⊢ (((𝐶 ∈ N ∧
𝐷 ∈ N)
∧ (𝑅 ∈
N ∧ 𝑆
∈ N)) → ((𝐶 ·N 𝑅) ∈ N ∧
(𝐷
·N 𝑆) ∈ N)) |
10 | 5, 9 | anim12i 321 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐹 ∈
N ∧ 𝐺
∈ N)) ∧ ((𝐶 ∈ N ∧ 𝐷 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·N 𝐹) ∈ N ∧
(𝐵
·N 𝐺) ∈ N) ∧ ((𝐶
·N 𝑅) ∈ N ∧ (𝐷
·N 𝑆) ∈ N))) |
11 | 10 | an4s 522 |
. . . 4
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·N 𝐹) ∈ N ∧
(𝐵
·N 𝐺) ∈ N) ∧ ((𝐶
·N 𝑅) ∈ N ∧ (𝐷
·N 𝑆) ∈ N))) |
12 | | enqbreq 6454 |
. . . 4
⊢ ((((𝐴
·N 𝐹) ∈ N ∧ (𝐵
·N 𝐺) ∈ N) ∧ ((𝐶
·N 𝑅) ∈ N ∧ (𝐷
·N 𝑆) ∈ N)) →
(〈(𝐴
·N 𝐹), (𝐵 ·N 𝐺)〉
~Q 〈(𝐶 ·N 𝑅), (𝐷 ·N 𝑆)〉 ↔ ((𝐴
·N 𝐹) ·N (𝐷
·N 𝑆)) = ((𝐵 ·N 𝐺)
·N (𝐶 ·N 𝑅)))) |
13 | 11, 12 | syl 14 |
. . 3
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (〈(𝐴 ·N 𝐹), (𝐵 ·N 𝐺)〉
~Q 〈(𝐶 ·N 𝑅), (𝐷 ·N 𝑆)〉 ↔ ((𝐴
·N 𝐹) ·N (𝐷
·N 𝑆)) = ((𝐵 ·N 𝐺)
·N (𝐶 ·N 𝑅)))) |
14 | | simplll 485 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝐴
∈ N) |
15 | | simprll 489 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝐹
∈ N) |
16 | | simplrr 488 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝐷
∈ N) |
17 | | mulcompig 6429 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ (𝑥
·N 𝑦) = (𝑦 ·N 𝑥)) |
18 | 17 | adantl 262 |
. . . . 5
⊢
(((((𝐴 ∈
N ∧ 𝐵
∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) ∧
((𝐹 ∈ N
∧ 𝐺 ∈
N) ∧ (𝑅
∈ N ∧ 𝑆 ∈ N))) ∧ (𝑥 ∈ N ∧
𝑦 ∈ N))
→ (𝑥
·N 𝑦) = (𝑦 ·N 𝑥)) |
19 | | mulasspig 6430 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N) → ((𝑥
·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦
·N 𝑧))) |
20 | 19 | adantl 262 |
. . . . 5
⊢
(((((𝐴 ∈
N ∧ 𝐵
∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) ∧
((𝐹 ∈ N
∧ 𝐺 ∈
N) ∧ (𝑅
∈ N ∧ 𝑆 ∈ N))) ∧ (𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N)) → ((𝑥 ·N 𝑦)
·N 𝑧) = (𝑥 ·N (𝑦
·N 𝑧))) |
21 | | simprrr 492 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝑆
∈ N) |
22 | | mulclpi 6426 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ (𝑥
·N 𝑦) ∈ N) |
23 | 22 | adantl 262 |
. . . . 5
⊢
(((((𝐴 ∈
N ∧ 𝐵
∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) ∧
((𝐹 ∈ N
∧ 𝐺 ∈
N) ∧ (𝑅
∈ N ∧ 𝑆 ∈ N))) ∧ (𝑥 ∈ N ∧
𝑦 ∈ N))
→ (𝑥
·N 𝑦) ∈ N) |
24 | 14, 15, 16, 18, 20, 21, 23 | caov4d 5685 |
. . . 4
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → ((𝐴 ·N 𝐹)
·N (𝐷 ·N 𝑆)) = ((𝐴 ·N 𝐷)
·N (𝐹 ·N 𝑆))) |
25 | | simpllr 486 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝐵
∈ N) |
26 | | simprlr 490 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝐺
∈ N) |
27 | | simplrl 487 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝐶
∈ N) |
28 | | simprrl 491 |
. . . . 5
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → 𝑅
∈ N) |
29 | 25, 26, 27, 18, 20, 28, 23 | caov4d 5685 |
. . . 4
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → ((𝐵 ·N 𝐺)
·N (𝐶 ·N 𝑅)) = ((𝐵 ·N 𝐶)
·N (𝐺 ·N 𝑅))) |
30 | 24, 29 | eqeq12d 2054 |
. . 3
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·N 𝐹)
·N (𝐷 ·N 𝑆)) = ((𝐵 ·N 𝐺)
·N (𝐶 ·N 𝑅)) ↔ ((𝐴 ·N 𝐷)
·N (𝐹 ·N 𝑆)) = ((𝐵 ·N 𝐶)
·N (𝐺 ·N 𝑅)))) |
31 | 13, 30 | bitrd 177 |
. 2
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (〈(𝐴 ·N 𝐹), (𝐵 ·N 𝐺)〉
~Q 〈(𝐶 ·N 𝑅), (𝐷 ·N 𝑆)〉 ↔ ((𝐴
·N 𝐷) ·N (𝐹
·N 𝑆)) = ((𝐵 ·N 𝐶)
·N (𝐺 ·N 𝑅)))) |
32 | 1, 31 | syl5ibr 145 |
1
⊢ ((((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐶 ∈
N ∧ 𝐷
∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → 〈(𝐴
·N 𝐹), (𝐵 ·N 𝐺)〉
~Q 〈(𝐶 ·N 𝑅), (𝐷 ·N 𝑆)〉)) |