Step | Hyp | Ref
| Expression |
1 | | df-nq0 7380 |
. 2
⊢
Q0 = ((ω × N)
/ ~Q0 ) |
2 | | oveq1 5858 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~Q0 = 𝐴 → ([〈𝑥, 𝑦〉] ~Q0
·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
(𝐴
·Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
3 | | oveq2 5859 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~Q0 = 𝐴 → ([〈𝑧, 𝑤〉] ~Q0
·Q0 [〈𝑥, 𝑦〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 ·Q0 𝐴)) |
4 | 2, 3 | eqeq12d 2185 |
. 2
⊢
([〈𝑥, 𝑦〉]
~Q0 = 𝐴 → (([〈𝑥, 𝑦〉] ~Q0
·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 ·Q0 [〈𝑥, 𝑦〉] ~Q0 ) ↔
(𝐴
·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 ·Q0 𝐴))) |
5 | | oveq2 5859 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~Q0 = 𝐵 → (𝐴 ·Q0
[〈𝑧, 𝑤〉]
~Q0 ) = (𝐴 ·Q0 𝐵)) |
6 | | oveq1 5858 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~Q0 = 𝐵 → ([〈𝑧, 𝑤〉] ~Q0
·Q0 𝐴) = (𝐵 ·Q0 𝐴)) |
7 | 5, 6 | eqeq12d 2185 |
. 2
⊢
([〈𝑧, 𝑤〉]
~Q0 = 𝐵 → ((𝐴 ·Q0
[〈𝑧, 𝑤〉]
~Q0 ) = ([〈𝑧, 𝑤〉] ~Q0
·Q0 𝐴) ↔ (𝐴 ·Q0 𝐵) = (𝐵 ·Q0 𝐴))) |
8 | | nnmcom 6466 |
. . . . 5
⊢ ((𝑥 ∈ ω ∧ 𝑧 ∈ ω) → (𝑥 ·o 𝑧) = (𝑧 ·o 𝑥)) |
9 | 8 | ad2ant2r 506 |
. . . 4
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ (𝑥
·o 𝑧) =
(𝑧 ·o
𝑥)) |
10 | | pinn 7264 |
. . . . . 6
⊢ (𝑦 ∈ N →
𝑦 ∈
ω) |
11 | | pinn 7264 |
. . . . . 6
⊢ (𝑤 ∈ N →
𝑤 ∈
ω) |
12 | | nnmcom 6466 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ 𝑤 ∈ ω) → (𝑦 ·o 𝑤) = (𝑤 ·o 𝑦)) |
13 | 10, 11, 12 | syl2an 287 |
. . . . 5
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·o 𝑤) =
(𝑤 ·o
𝑦)) |
14 | 13 | ad2ant2l 505 |
. . . 4
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ (𝑦
·o 𝑤) =
(𝑤 ·o
𝑦)) |
15 | | opeq12 3765 |
. . . . 5
⊢ (((𝑥 ·o 𝑧) = (𝑧 ·o 𝑥) ∧ (𝑦 ·o 𝑤) = (𝑤 ·o 𝑦)) → 〈(𝑥 ·o 𝑧), (𝑦 ·o 𝑤)〉 = 〈(𝑧 ·o 𝑥), (𝑤 ·o 𝑦)〉) |
16 | 15 | eceq1d 6547 |
. . . 4
⊢ (((𝑥 ·o 𝑧) = (𝑧 ·o 𝑥) ∧ (𝑦 ·o 𝑤) = (𝑤 ·o 𝑦)) → [〈(𝑥 ·o 𝑧), (𝑦 ·o 𝑤)〉] ~Q0 =
[〈(𝑧
·o 𝑥),
(𝑤 ·o
𝑦)〉]
~Q0 ) |
17 | 9, 14, 16 | syl2anc 409 |
. . 3
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ [〈(𝑥
·o 𝑧),
(𝑦 ·o
𝑤)〉]
~Q0 = [〈(𝑧 ·o 𝑥), (𝑤 ·o 𝑦)〉] ~Q0
) |
18 | | mulnnnq0 7405 |
. . 3
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ ([〈𝑥, 𝑦〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈(𝑥
·o 𝑧),
(𝑦 ·o
𝑤)〉]
~Q0 ) |
19 | | mulnnnq0 7405 |
. . . 4
⊢ (((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧
(𝑥 ∈ ω ∧
𝑦 ∈ N))
→ ([〈𝑧, 𝑤〉]
~Q0 ·Q0 [〈𝑥, 𝑦〉] ~Q0 ) =
[〈(𝑧
·o 𝑥),
(𝑤 ·o
𝑦)〉]
~Q0 ) |
20 | 19 | ancoms 266 |
. . 3
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ ([〈𝑧, 𝑤〉]
~Q0 ·Q0 [〈𝑥, 𝑦〉] ~Q0 ) =
[〈(𝑧
·o 𝑥),
(𝑤 ·o
𝑦)〉]
~Q0 ) |
21 | 17, 18, 20 | 3eqtr4d 2213 |
. 2
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ ([〈𝑥, 𝑦〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 ·Q0 [〈𝑥, 𝑦〉] ~Q0
)) |
22 | 1, 4, 7, 21 | 2ecoptocl 6599 |
1
⊢ ((𝐴 ∈
Q0 ∧ 𝐵 ∈ Q0) →
(𝐴
·Q0 𝐵) = (𝐵 ·Q0 𝐴)) |