Step | Hyp | Ref
| Expression |
1 | | df-nq0 6408 |
. . . 4
⊢
Q0 = ((𝜔 × N)
/ ~Q0 ) |
2 | | oveq1 5462 |
. . . . . . 7
⊢
([〈z, w〉] ~Q0 = B → ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 ) = (B
+Q0 [〈v,
u〉] ~Q0
)) |
3 | 2 | oveq2d 5471 |
. . . . . 6
⊢
([〈z, w〉] ~Q0 = B → (A
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = (A
·Q0 (B
+Q0 [〈v,
u〉] ~Q0
))) |
4 | | oveq2 5463 |
. . . . . . 7
⊢
([〈z, w〉] ~Q0 = B → (A
·Q0 [〈z, w〉]
~Q0 ) = (A
·Q0 B)) |
5 | 4 | oveq1d 5470 |
. . . . . 6
⊢
([〈z, w〉] ~Q0 = B → ((A
·Q0 [〈z, w〉]
~Q0 ) +Q0 (A ·Q0
[〈v, u〉] ~Q0 )) =
((A ·Q0
B) +Q0 (A ·Q0
[〈v, u〉] ~Q0
))) |
6 | 3, 5 | eqeq12d 2051 |
. . . . 5
⊢
([〈z, w〉] ~Q0 = B → ((A
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = ((A
·Q0 [〈z, w〉]
~Q0 ) +Q0 (A ·Q0
[〈v, u〉] ~Q0 )) ↔
(A ·Q0
(B +Q0
[〈v, u〉] ~Q0 )) =
((A ·Q0
B) +Q0 (A ·Q0
[〈v, u〉] ~Q0
)))) |
7 | 6 | imbi2d 219 |
. . . 4
⊢
([〈z, w〉] ~Q0 = B → ((A
∈ Q0 →
(A ·Q0
([〈z, w〉] ~Q0
+Q0 [〈v,
u〉] ~Q0 )) =
((A ·Q0
[〈z, w〉] ~Q0 )
+Q0 (A
·Q0 [〈v, u〉]
~Q0 ))) ↔ (A
∈ Q0 →
(A ·Q0
(B +Q0
[〈v, u〉] ~Q0 )) =
((A ·Q0
B) +Q0 (A ·Q0
[〈v, u〉] ~Q0
))))) |
8 | | oveq2 5463 |
. . . . . . 7
⊢
([〈v, u〉] ~Q0 = 𝐶 → (B +Q0 [〈v, u〉]
~Q0 ) = (B
+Q0 𝐶)) |
9 | 8 | oveq2d 5471 |
. . . . . 6
⊢
([〈v, u〉] ~Q0 = 𝐶 → (A ·Q0 (B +Q0 [〈v, u〉]
~Q0 )) = (A
·Q0 (B
+Q0 𝐶))) |
10 | | oveq2 5463 |
. . . . . . 7
⊢
([〈v, u〉] ~Q0 = 𝐶 → (A ·Q0
[〈v, u〉] ~Q0 ) = (A ·Q0 𝐶)) |
11 | 10 | oveq2d 5471 |
. . . . . 6
⊢
([〈v, u〉] ~Q0 = 𝐶 → ((A ·Q0 B) +Q0 (A ·Q0
[〈v, u〉] ~Q0 )) =
((A ·Q0
B) +Q0 (A ·Q0 𝐶))) |
12 | 9, 11 | eqeq12d 2051 |
. . . . 5
⊢
([〈v, u〉] ~Q0 = 𝐶 → ((A ·Q0 (B +Q0 [〈v, u〉]
~Q0 )) = ((A
·Q0 B)
+Q0 (A
·Q0 [〈v, u〉]
~Q0 )) ↔ (A
·Q0 (B
+Q0 𝐶)) = ((A
·Q0 B)
+Q0 (A
·Q0 𝐶)))) |
13 | 12 | imbi2d 219 |
. . . 4
⊢
([〈v, u〉] ~Q0 = 𝐶 → ((A ∈
Q0 → (A
·Q0 (B
+Q0 [〈v,
u〉] ~Q0 )) =
((A ·Q0
B) +Q0 (A ·Q0
[〈v, u〉] ~Q0 ))) ↔
(A ∈
Q0 → (A
·Q0 (B
+Q0 𝐶)) = ((A
·Q0 B)
+Q0 (A
·Q0 𝐶))))) |
14 | | oveq1 5462 |
. . . . . . . 8
⊢
([〈x, y〉] ~Q0 = A → ([〈x, y〉]
~Q0 ·Q0
([〈z, w〉] ~Q0
+Q0 [〈v,
u〉] ~Q0 )) =
(A ·Q0
([〈z, w〉] ~Q0
+Q0 [〈v,
u〉] ~Q0
))) |
15 | | oveq1 5462 |
. . . . . . . . 9
⊢
([〈x, y〉] ~Q0 = A → ([〈x, y〉]
~Q0 ·Q0
[〈z, w〉] ~Q0 ) = (A ·Q0
[〈z, w〉] ~Q0
)) |
16 | | oveq1 5462 |
. . . . . . . . 9
⊢
([〈x, y〉] ~Q0 = A → ([〈x, y〉]
~Q0 ·Q0
[〈v, u〉] ~Q0 ) = (A ·Q0
[〈v, u〉] ~Q0
)) |
17 | 15, 16 | oveq12d 5473 |
. . . . . . . 8
⊢
([〈x, y〉] ~Q0 = A → (([〈x, y〉]
~Q0 ·Q0
[〈z, w〉] ~Q0 )
+Q0 ([〈x,
y〉] ~Q0
·Q0 [〈v, u〉]
~Q0 )) = ((A
·Q0 [〈z, w〉]
~Q0 ) +Q0 (A ·Q0
[〈v, u〉] ~Q0
))) |
18 | 14, 17 | eqeq12d 2051 |
. . . . . . 7
⊢
([〈x, y〉] ~Q0 = A → (([〈x, y〉]
~Q0 ·Q0
([〈z, w〉] ~Q0
+Q0 [〈v,
u〉] ~Q0 )) =
(([〈x, y〉] ~Q0
·Q0 [〈z, w〉]
~Q0 ) +Q0 ([〈x, y〉]
~Q0 ·Q0
[〈v, u〉] ~Q0 )) ↔
(A ·Q0
([〈z, w〉] ~Q0
+Q0 [〈v,
u〉] ~Q0 )) =
((A ·Q0
[〈z, w〉] ~Q0 )
+Q0 (A
·Q0 [〈v, u〉]
~Q0 )))) |
19 | 18 | imbi2d 219 |
. . . . . 6
⊢
([〈x, y〉] ~Q0 = A → ((((z
∈ 𝜔 ∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → ([〈x,
y〉] ~Q0
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = (([〈x, y〉]
~Q0 ·Q0
[〈z, w〉] ~Q0 )
+Q0 ([〈x,
y〉] ~Q0
·Q0 [〈v, u〉]
~Q0 ))) ↔ (((z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → (A
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = ((A
·Q0 [〈z, w〉]
~Q0 ) +Q0 (A ·Q0
[〈v, u〉] ~Q0
))))) |
20 | | an42 521 |
. . . . . . . . . . . 12
⊢
(((z ∈ 𝜔 ∧
u ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
↔ ((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N))) |
21 | 20 | anbi2i 430 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ ((z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔))) ↔ ((x ∈ 𝜔
∧ y ∈ N) ∧ ((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)))) |
22 | | 3anass 888 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) ↔ ((x ∈ 𝜔
∧ y ∈ N) ∧ ((z ∈ 𝜔 ∧
u ∈
N) ∧ (w ∈
N ∧ v ∈
𝜔)))) |
23 | | 3anass 888 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) ↔ ((x ∈ 𝜔 ∧
y ∈
N) ∧ ((z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)))) |
24 | 21, 22, 23 | 3bitr4i 201 |
. . . . . . . . . 10
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) ↔ ((x ∈ 𝜔
∧ y ∈ N) ∧ (z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N))) |
25 | | pinn 6293 |
. . . . . . . . . . . . . 14
⊢ (y ∈
N → y ∈ 𝜔) |
26 | | nnmcl 5999 |
. . . . . . . . . . . . . 14
⊢
((y ∈ 𝜔 ∧
x ∈
𝜔) → (y
·𝑜 x) ∈ 𝜔) |
27 | 25, 26 | sylan 267 |
. . . . . . . . . . . . 13
⊢
((y ∈ N ∧ x ∈ 𝜔) → (y ·𝑜 x) ∈
𝜔) |
28 | 27 | ancoms 255 |
. . . . . . . . . . . 12
⊢
((x ∈ 𝜔 ∧
y ∈
N) → (y
·𝑜 x) ∈ 𝜔) |
29 | | pinn 6293 |
. . . . . . . . . . . . 13
⊢ (u ∈
N → u ∈ 𝜔) |
30 | | nnmcl 5999 |
. . . . . . . . . . . . 13
⊢
((z ∈ 𝜔 ∧
u ∈
𝜔) → (z
·𝑜 u) ∈ 𝜔) |
31 | 29, 30 | sylan2 270 |
. . . . . . . . . . . 12
⊢
((z ∈ 𝜔 ∧
u ∈
N) → (z
·𝑜 u) ∈ 𝜔) |
32 | | pinn 6293 |
. . . . . . . . . . . . 13
⊢ (w ∈
N → w ∈ 𝜔) |
33 | | nnmcl 5999 |
. . . . . . . . . . . . 13
⊢
((w ∈ 𝜔 ∧
v ∈
𝜔) → (w
·𝑜 v) ∈ 𝜔) |
34 | 32, 33 | sylan 267 |
. . . . . . . . . . . 12
⊢
((w ∈ N ∧ v ∈ 𝜔) → (w ·𝑜 v) ∈
𝜔) |
35 | | nndi 6004 |
. . . . . . . . . . . 12
⊢
(((y ·𝑜
x) ∈
𝜔 ∧ (z ·𝑜 u) ∈ 𝜔
∧ (w
·𝑜 v) ∈ 𝜔) → ((y ·𝑜 x) ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) = (((y
·𝑜 x)
·𝑜 (z
·𝑜 u))
+𝑜 ((y
·𝑜 x)
·𝑜 (w
·𝑜 v)))) |
36 | 28, 31, 34, 35 | syl3an 1176 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → ((y ·𝑜 x) ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) = (((y
·𝑜 x)
·𝑜 (z
·𝑜 u))
+𝑜 ((y
·𝑜 x)
·𝑜 (w
·𝑜 v)))) |
37 | | simp1r 928 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → y ∈
N) |
38 | | simp1l 927 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → x ∈
𝜔) |
39 | 31 | 3ad2ant2 925 |
. . . . . . . . . . . . 13
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (z ·𝑜 u) ∈
𝜔) |
40 | 34 | 3ad2ant3 926 |
. . . . . . . . . . . . 13
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (w ·𝑜 v) ∈
𝜔) |
41 | | nnacl 5998 |
. . . . . . . . . . . . 13
⊢
(((z ·𝑜
u) ∈
𝜔 ∧ (w ·𝑜 v) ∈ 𝜔)
→ ((z ·𝑜
u) +𝑜 (w ·𝑜 v)) ∈
𝜔) |
42 | 39, 40, 41 | syl2anc 391 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → ((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈
𝜔) |
43 | | nnmass 6005 |
. . . . . . . . . . . . 13
⊢
((y ∈ 𝜔 ∧
x ∈
𝜔 ∧ ((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔)
→ ((y ·𝑜
x) ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) = (y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))))) |
44 | 25, 43 | syl3an1 1167 |
. . . . . . . . . . . 12
⊢
((y ∈ N ∧ x ∈ 𝜔 ∧
((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔)
→ ((y ·𝑜
x) ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) = (y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))))) |
45 | 37, 38, 42, 44 | syl3anc 1134 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → ((y ·𝑜 x) ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) = (y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))))) |
46 | | nnmcom 6007 |
. . . . . . . . . . . . . . . . 17
⊢
((x ∈ 𝜔 ∧
y ∈
𝜔) → (x
·𝑜 y) = (y ·𝑜 x)) |
47 | 25, 46 | sylan2 270 |
. . . . . . . . . . . . . . . 16
⊢
((x ∈ 𝜔 ∧
y ∈
N) → (x
·𝑜 y) = (y ·𝑜 x)) |
48 | 47 | oveq1d 5470 |
. . . . . . . . . . . . . . 15
⊢
((x ∈ 𝜔 ∧
y ∈
N) → ((x
·𝑜 y)
·𝑜 (z
·𝑜 u)) =
((y ·𝑜 x) ·𝑜 (z ·𝑜 u))) |
49 | 48 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → ((x ·𝑜 y) ·𝑜 (z ·𝑜 u)) = ((y
·𝑜 x)
·𝑜 (z
·𝑜 u))) |
50 | | simpll 481 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → x ∈
𝜔) |
51 | 25 | ad2antlr 458 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → y ∈
𝜔) |
52 | | simprl 483 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → z ∈
𝜔) |
53 | | nnmcom 6007 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ 𝜔 ∧
g ∈
𝜔) → (f
·𝑜 g) = (g ·𝑜 f)) |
54 | 53 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) ∧ (f ∈ 𝜔 ∧
g ∈
𝜔)) → (f
·𝑜 g) = (g ·𝑜 f)) |
55 | | nnmass 6005 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ 𝜔 ∧
g ∈
𝜔 ∧ ℎ ∈
𝜔) → ((f
·𝑜 g)
·𝑜 ℎ)
= (f ·𝑜 (g ·𝑜 ℎ))) |
56 | 55 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) ∧ (f ∈ 𝜔 ∧
g ∈
𝜔 ∧ ℎ ∈
𝜔)) → ((f
·𝑜 g)
·𝑜 ℎ)
= (f ·𝑜 (g ·𝑜 ℎ))) |
57 | | simprr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → u ∈
N) |
58 | 57, 29 | syl 14 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → u ∈
𝜔) |
59 | | nnmcl 5999 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ 𝜔 ∧
g ∈
𝜔) → (f
·𝑜 g) ∈ 𝜔) |
60 | 59 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) ∧ (f ∈ 𝜔 ∧
g ∈
𝜔)) → (f
·𝑜 g) ∈ 𝜔) |
61 | 50, 51, 52, 54, 56, 58, 60 | caov4d 5627 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → ((x ·𝑜 y) ·𝑜 (z ·𝑜 u)) = ((x
·𝑜 z)
·𝑜 (y
·𝑜 u))) |
62 | 49, 61 | eqtr3d 2071 |
. . . . . . . . . . . . 13
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N)) → ((y ·𝑜 x) ·𝑜 (z ·𝑜 u)) = ((x
·𝑜 z)
·𝑜 (y
·𝑜 u))) |
63 | 62 | 3adant3 923 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → ((y ·𝑜 x) ·𝑜 (z ·𝑜 u)) = ((x
·𝑜 z)
·𝑜 (y
·𝑜 u))) |
64 | 25 | ad2antlr 458 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ y ∈ 𝜔) |
65 | | simpll 481 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ x ∈ 𝜔) |
66 | | simprl 483 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ w ∈ N) |
67 | 66, 32 | syl 14 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ w ∈ 𝜔) |
68 | 53 | adantl 262 |
. . . . . . . . . . . . . 14
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
∧ (f ∈ 𝜔 ∧
g ∈
𝜔)) → (f
·𝑜 g) = (g ·𝑜 f)) |
69 | 55 | adantl 262 |
. . . . . . . . . . . . . 14
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
∧ (f ∈ 𝜔 ∧
g ∈
𝜔 ∧ ℎ ∈
𝜔)) → ((f
·𝑜 g)
·𝑜 ℎ)
= (f ·𝑜 (g ·𝑜 ℎ))) |
70 | | simprr 484 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ v ∈ 𝜔) |
71 | 59 | adantl 262 |
. . . . . . . . . . . . . 14
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
∧ (f ∈ 𝜔 ∧
g ∈
𝜔)) → (f
·𝑜 g) ∈ 𝜔) |
72 | 64, 65, 67, 68, 69, 70, 71 | caov4d 5627 |
. . . . . . . . . . . . 13
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ ((y ·𝑜
x) ·𝑜 (w ·𝑜 v)) = ((y
·𝑜 w)
·𝑜 (x
·𝑜 v))) |
73 | 72 | 3adant2 922 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → ((y ·𝑜 x) ·𝑜 (w ·𝑜 v)) = ((y
·𝑜 w)
·𝑜 (x
·𝑜 v))) |
74 | 63, 73 | oveq12d 5473 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (((y ·𝑜 x) ·𝑜 (z ·𝑜 u)) +𝑜 ((y ·𝑜 x) ·𝑜 (w ·𝑜 v))) = (((x
·𝑜 z)
·𝑜 (y
·𝑜 u))
+𝑜 ((y
·𝑜 w)
·𝑜 (x
·𝑜 v)))) |
75 | 36, 45, 74 | 3eqtr3d 2077 |
. . . . . . . . . 10
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (y ·𝑜 (x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v)))) = (((x
·𝑜 z)
·𝑜 (y
·𝑜 u))
+𝑜 ((y
·𝑜 w)
·𝑜 (x
·𝑜 v)))) |
76 | 24, 75 | sylbir 125 |
. . . . . . . . 9
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → (y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v)))) =
(((x ·𝑜 z) ·𝑜 (y ·𝑜 u)) +𝑜 ((y ·𝑜 w) ·𝑜 (x ·𝑜 v)))) |
77 | 37, 25 | syl 14 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → y ∈
𝜔) |
78 | | mulpiord 6301 |
. . . . . . . . . . . . . . . 16
⊢
((w ∈ N ∧ u ∈ N) → (w ·N u) = (w
·𝑜 u)) |
79 | 78 | ancoms 255 |
. . . . . . . . . . . . . . 15
⊢
((u ∈ N ∧ w ∈ N) → (w ·N u) = (w
·𝑜 u)) |
80 | 79 | ad2ant2lr 479 |
. . . . . . . . . . . . . 14
⊢
(((z ∈ 𝜔 ∧
u ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ (w
·N u) =
(w ·𝑜 u)) |
81 | 80 | 3adant1 921 |
. . . . . . . . . . . . 13
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (w ·N u) = (w
·𝑜 u)) |
82 | 66 | 3adant2 922 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → w ∈
N) |
83 | 57 | 3adant3 923 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → u ∈
N) |
84 | | mulclpi 6312 |
. . . . . . . . . . . . . . 15
⊢
((w ∈ N ∧ u ∈ N) → (w ·N u) ∈
N) |
85 | 82, 83, 84 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (w ·N u) ∈
N) |
86 | | pinn 6293 |
. . . . . . . . . . . . . 14
⊢
((w
·N u) ∈ N → (w ·N u) ∈
𝜔) |
87 | 85, 86 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (w ·N u) ∈
𝜔) |
88 | 81, 87 | eqeltrrd 2112 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (w ·𝑜 u) ∈
𝜔) |
89 | | nnmass 6005 |
. . . . . . . . . . . 12
⊢
((y ∈ 𝜔 ∧
y ∈
𝜔 ∧ (w ·𝑜 u) ∈ 𝜔)
→ ((y ·𝑜
y) ·𝑜 (w ·𝑜 u)) = (y
·𝑜 (y
·𝑜 (w
·𝑜 u)))) |
90 | 77, 77, 88, 89 | syl3anc 1134 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → ((y ·𝑜 y) ·𝑜 (w ·𝑜 u)) = (y
·𝑜 (y
·𝑜 (w
·𝑜 u)))) |
91 | 82, 32 | syl 14 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → w ∈
𝜔) |
92 | 53 | adantl 262 |
. . . . . . . . . . . 12
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) ∧
(f ∈
𝜔 ∧ g ∈ 𝜔))
→ (f ·𝑜
g) = (g
·𝑜 f)) |
93 | 55 | adantl 262 |
. . . . . . . . . . . 12
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) ∧
(f ∈
𝜔 ∧ g ∈ 𝜔
∧ ℎ ∈
𝜔)) → ((f
·𝑜 g)
·𝑜 ℎ)
= (f ·𝑜 (g ·𝑜 ℎ))) |
94 | 83, 29 | syl 14 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → u ∈
𝜔) |
95 | 59 | adantl 262 |
. . . . . . . . . . . 12
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) ∧
(f ∈
𝜔 ∧ g ∈ 𝜔))
→ (f ·𝑜
g) ∈
𝜔) |
96 | 77, 77, 91, 92, 93, 94, 95 | caov4d 5627 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → ((y ·𝑜 y) ·𝑜 (w ·𝑜 u)) = ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))) |
97 | 90, 96 | eqtr3d 2071 |
. . . . . . . . . 10
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ u ∈ N) ∧ (w ∈ N ∧ v ∈ 𝜔)) → (y ·𝑜 (y ·𝑜 (w ·𝑜 u))) = ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))) |
98 | 24, 97 | sylbir 125 |
. . . . . . . . 9
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → (y
·𝑜 (y
·𝑜 (w
·𝑜 u))) =
((y ·𝑜 w) ·𝑜 (y ·𝑜 u))) |
99 | | opeq12 3542 |
. . . . . . . . . 10
⊢
(((y ·𝑜
(x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v)))) = (((x
·𝑜 z)
·𝑜 (y
·𝑜 u))
+𝑜 ((y
·𝑜 w)
·𝑜 (x
·𝑜 v))) ∧ (y
·𝑜 (y
·𝑜 (w
·𝑜 u))) =
((y ·𝑜 w) ·𝑜 (y ·𝑜 u))) → 〈(y ·𝑜 (x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v)))), (y
·𝑜 (y
·𝑜 (w
·𝑜 u)))〉 =
〈(((x ·𝑜
z) ·𝑜 (y ·𝑜 u)) +𝑜 ((y ·𝑜 w) ·𝑜 (x ·𝑜 v))), ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))〉) |
100 | 99 | eceq1d 6078 |
. . . . . . . . 9
⊢
(((y ·𝑜
(x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v)))) = (((x
·𝑜 z)
·𝑜 (y
·𝑜 u))
+𝑜 ((y
·𝑜 w)
·𝑜 (x
·𝑜 v))) ∧ (y
·𝑜 (y
·𝑜 (w
·𝑜 u))) =
((y ·𝑜 w) ·𝑜 (y ·𝑜 u))) → [〈(y ·𝑜 (x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v)))), (y
·𝑜 (y
·𝑜 (w
·𝑜 u)))〉]
~Q0 = [〈(((x
·𝑜 z)
·𝑜 (y
·𝑜 u))
+𝑜 ((y
·𝑜 w)
·𝑜 (x
·𝑜 v))),
((y ·𝑜 w) ·𝑜 (y ·𝑜 u))〉] ~Q0
) |
101 | 76, 98, 100 | syl2anc 391 |
. . . . . . . 8
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → [〈(y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v)))),
(y ·𝑜 (y ·𝑜 (w ·𝑜 u)))〉] ~Q0 =
[〈(((x ·𝑜
z) ·𝑜 (y ·𝑜 u)) +𝑜 ((y ·𝑜 w) ·𝑜 (x ·𝑜 v))), ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))〉]
~Q0 ) |
102 | | addnnnq0 6432 |
. . . . . . . . . . . 12
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 ) = [〈((z
·𝑜 u)
+𝑜 (w
·𝑜 v)), (w ·𝑜 u)〉] ~Q0
) |
103 | 102 | oveq2d 5471 |
. . . . . . . . . . 11
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → ([〈x, y〉]
~Q0 ·Q0
([〈z, w〉] ~Q0
+Q0 [〈v,
u〉] ~Q0 )) =
([〈x, y〉] ~Q0
·Q0 [〈((z ·𝑜 u) +𝑜 (w ·𝑜 v)), (w
·𝑜 u)〉]
~Q0 )) |
104 | 103 | adantl 262 |
. . . . . . . . . 10
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ ((z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N))) → ([〈x,
y〉] ~Q0
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = ([〈x, y〉]
~Q0 ·Q0
[〈((z ·𝑜
u) +𝑜 (w ·𝑜 v)), (w
·𝑜 u)〉]
~Q0 )) |
105 | 31, 34, 41 | syl2an 273 |
. . . . . . . . . . . . 13
⊢
(((z ∈ 𝜔 ∧
u ∈
N) ∧ (w ∈
N ∧ v ∈ 𝜔))
→ ((z ·𝑜
u) +𝑜 (w ·𝑜 v)) ∈
𝜔) |
106 | 105 | an42s 523 |
. . . . . . . . . . . 12
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → ((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈
𝜔) |
107 | 84 | ad2ant2l 477 |
. . . . . . . . . . . . 13
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → (w ·N u) ∈
N) |
108 | 78 | eleq1d 2103 |
. . . . . . . . . . . . . 14
⊢
((w ∈ N ∧ u ∈ N) → ((w ·N u) ∈
N ↔ (w
·𝑜 u) ∈ N)) |
109 | 108 | ad2ant2l 477 |
. . . . . . . . . . . . 13
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → ((w ·N u) ∈
N ↔ (w
·𝑜 u) ∈ N)) |
110 | 107, 109 | mpbid 135 |
. . . . . . . . . . . 12
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → (w ·𝑜 u) ∈
N) |
111 | 106, 110 | jca 290 |
. . . . . . . . . . 11
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → (((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔
∧ (w
·𝑜 u) ∈ N)) |
112 | | mulnnnq0 6433 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔
∧ (w
·𝑜 u) ∈ N)) → ([〈x, y〉]
~Q0 ·Q0
[〈((z ·𝑜
u) +𝑜 (w ·𝑜 v)), (w
·𝑜 u)〉]
~Q0 ) = [〈(x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))),
(y ·𝑜 (w ·𝑜 u))〉] ~Q0
) |
113 | | nnmcl 5999 |
. . . . . . . . . . . . . . . 16
⊢
((x ∈ 𝜔 ∧
((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔)
→ (x ·𝑜
((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈
𝜔) |
114 | | simpl 102 |
. . . . . . . . . . . . . . . . 17
⊢
((y ∈ N ∧ (w
·𝑜 u) ∈ N) → y ∈
N) |
115 | | mulpiord 6301 |
. . . . . . . . . . . . . . . . . 18
⊢
((y ∈ N ∧ (w
·𝑜 u) ∈ N) → (y ·N (w ·𝑜 u)) = (y
·𝑜 (w
·𝑜 u))) |
116 | | mulclpi 6312 |
. . . . . . . . . . . . . . . . . 18
⊢
((y ∈ N ∧ (w
·𝑜 u) ∈ N) → (y ·N (w ·𝑜 u)) ∈
N) |
117 | 115, 116 | eqeltrrd 2112 |
. . . . . . . . . . . . . . . . 17
⊢
((y ∈ N ∧ (w
·𝑜 u) ∈ N) → (y ·𝑜 (w ·𝑜 u)) ∈
N) |
118 | 114, 117 | jca 290 |
. . . . . . . . . . . . . . . 16
⊢
((y ∈ N ∧ (w
·𝑜 u) ∈ N) → (y ∈
N ∧ (y ·𝑜 (w ·𝑜 u)) ∈
N)) |
119 | 113, 118 | anim12i 321 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ 𝜔 ∧
((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔)
∧ (y ∈ N ∧ (w
·𝑜 u) ∈ N)) → ((x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈ 𝜔
∧ (y ∈ N ∧ (y
·𝑜 (w
·𝑜 u)) ∈ N))) |
120 | | an12 495 |
. . . . . . . . . . . . . . . 16
⊢
(((x ·𝑜
((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈ 𝜔
∧ (y ∈ N ∧ (y
·𝑜 (w
·𝑜 u)) ∈ N)) ↔ (y ∈
N ∧ ((x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈ 𝜔
∧ (y
·𝑜 (w
·𝑜 u)) ∈ N))) |
121 | | 3anass 888 |
. . . . . . . . . . . . . . . 16
⊢
((y ∈ N ∧ (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))) ∈ 𝜔 ∧
(y ·𝑜 (w ·𝑜 u)) ∈
N) ↔ (y ∈ N ∧ ((x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))) ∈ 𝜔 ∧
(y ·𝑜 (w ·𝑜 u)) ∈
N))) |
122 | 120, 121 | bitr4i 176 |
. . . . . . . . . . . . . . 15
⊢
(((x ·𝑜
((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈ 𝜔
∧ (y ∈ N ∧ (y
·𝑜 (w
·𝑜 u)) ∈ N)) ↔ (y ∈
N ∧ (x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈ 𝜔
∧ (y
·𝑜 (w
·𝑜 u)) ∈ N)) |
123 | 119, 122 | sylib 127 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ 𝜔 ∧
((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔)
∧ (y ∈ N ∧ (w
·𝑜 u) ∈ N)) → (y ∈
N ∧ (x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈ 𝜔
∧ (y
·𝑜 (w
·𝑜 u)) ∈ N)) |
124 | 123 | an4s 522 |
. . . . . . . . . . . . 13
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔
∧ (w
·𝑜 u) ∈ N)) → (y ∈
N ∧ (x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v))) ∈ 𝜔
∧ (y
·𝑜 (w
·𝑜 u)) ∈ N)) |
125 | | mulcanenq0ec 6428 |
. . . . . . . . . . . . 13
⊢
((y ∈ N ∧ (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))) ∈ 𝜔 ∧
(y ·𝑜 (w ·𝑜 u)) ∈
N) → [〈(y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v)))),
(y ·𝑜 (y ·𝑜 (w ·𝑜 u)))〉] ~Q0 =
[〈(x ·𝑜
((z ·𝑜 u) +𝑜 (w ·𝑜 v))), (y
·𝑜 (w
·𝑜 u))〉]
~Q0 ) |
126 | 124, 125 | syl 14 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔
∧ (w
·𝑜 u) ∈ N)) → [〈(y ·𝑜 (x ·𝑜 ((z ·𝑜 u) +𝑜 (w ·𝑜 v)))), (y
·𝑜 (y
·𝑜 (w
·𝑜 u)))〉]
~Q0 = [〈(x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v))),
(y ·𝑜 (w ·𝑜 u))〉] ~Q0
) |
127 | 112, 126 | eqtr4d 2072 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (((z ·𝑜 u) +𝑜 (w ·𝑜 v)) ∈ 𝜔
∧ (w
·𝑜 u) ∈ N)) → ([〈x, y〉]
~Q0 ·Q0
[〈((z ·𝑜
u) +𝑜 (w ·𝑜 v)), (w
·𝑜 u)〉]
~Q0 ) = [〈(y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v)))),
(y ·𝑜 (y ·𝑜 (w ·𝑜 u)))〉] ~Q0
) |
128 | 111, 127 | sylan2 270 |
. . . . . . . . . 10
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ ((z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N))) → ([〈x,
y〉] ~Q0
·Q0 [〈((z ·𝑜 u) +𝑜 (w ·𝑜 v)), (w
·𝑜 u)〉]
~Q0 ) = [〈(y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v)))),
(y ·𝑜 (y ·𝑜 (w ·𝑜 u)))〉] ~Q0
) |
129 | 104, 128 | eqtrd 2069 |
. . . . . . . . 9
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ ((z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N))) → ([〈x,
y〉] ~Q0
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = [〈(y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v)))),
(y ·𝑜 (y ·𝑜 (w ·𝑜 u)))〉] ~Q0
) |
130 | 129 | 3impb 1099 |
. . . . . . . 8
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → ([〈x,
y〉] ~Q0
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = [〈(y
·𝑜 (x
·𝑜 ((z
·𝑜 u)
+𝑜 (w
·𝑜 v)))),
(y ·𝑜 (y ·𝑜 (w ·𝑜 u)))〉] ~Q0
) |
131 | | mulnnnq0 6433 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N)) → ([〈x, y〉]
~Q0 ·Q0
[〈z, w〉] ~Q0 ) =
[〈(x ·𝑜
z), (y
·𝑜 w)〉]
~Q0 ) |
132 | | mulnnnq0 6433 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → ([〈x, y〉]
~Q0 ·Q0
[〈v, u〉] ~Q0 ) =
[〈(x ·𝑜
v), (y
·𝑜 u)〉]
~Q0 ) |
133 | 131, 132 | oveqan12d 5474 |
. . . . . . . . . 10
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N)) ∧ ((x ∈ 𝜔 ∧
y ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N))) → (([〈x, y〉]
~Q0 ·Q0
[〈z, w〉] ~Q0 )
+Q0 ([〈x,
y〉] ~Q0
·Q0 [〈v, u〉]
~Q0 )) = ([〈(x ·𝑜 z), (y
·𝑜 w)〉]
~Q0 +Q0 [〈(x ·𝑜 v), (y
·𝑜 u)〉]
~Q0 )) |
134 | | nnmcl 5999 |
. . . . . . . . . . . . 13
⊢
((x ∈ 𝜔 ∧
z ∈
𝜔) → (x
·𝑜 z) ∈ 𝜔) |
135 | | mulpiord 6301 |
. . . . . . . . . . . . . 14
⊢
((y ∈ N ∧ w ∈ N) → (y ·N w) = (y
·𝑜 w)) |
136 | | mulclpi 6312 |
. . . . . . . . . . . . . 14
⊢
((y ∈ N ∧ w ∈ N) → (y ·N w) ∈
N) |
137 | 135, 136 | eqeltrrd 2112 |
. . . . . . . . . . . . 13
⊢
((y ∈ N ∧ w ∈ N) → (y ·𝑜 w) ∈
N) |
138 | 134, 137 | anim12i 321 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
z ∈
𝜔) ∧ (y ∈
N ∧ w ∈
N)) → ((x
·𝑜 z) ∈ 𝜔 ∧
(y ·𝑜 w) ∈
N)) |
139 | 138 | an4s 522 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N)) → ((x ·𝑜 z) ∈ 𝜔
∧ (y
·𝑜 w) ∈ N)) |
140 | | nnmcl 5999 |
. . . . . . . . . . . . 13
⊢
((x ∈ 𝜔 ∧
v ∈
𝜔) → (x
·𝑜 v) ∈ 𝜔) |
141 | | mulpiord 6301 |
. . . . . . . . . . . . . 14
⊢
((y ∈ N ∧ u ∈ N) → (y ·N u) = (y
·𝑜 u)) |
142 | | mulclpi 6312 |
. . . . . . . . . . . . . 14
⊢
((y ∈ N ∧ u ∈ N) → (y ·N u) ∈
N) |
143 | 141, 142 | eqeltrrd 2112 |
. . . . . . . . . . . . 13
⊢
((y ∈ N ∧ u ∈ N) → (y ·𝑜 u) ∈
N) |
144 | 140, 143 | anim12i 321 |
. . . . . . . . . . . 12
⊢
(((x ∈ 𝜔 ∧
v ∈
𝜔) ∧ (y ∈
N ∧ u ∈
N)) → ((x
·𝑜 v) ∈ 𝜔 ∧
(y ·𝑜 u) ∈
N)) |
145 | 144 | an4s 522 |
. . . . . . . . . . 11
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → ((x ·𝑜 v) ∈ 𝜔
∧ (y
·𝑜 u) ∈ N)) |
146 | | addnnnq0 6432 |
. . . . . . . . . . 11
⊢
((((x ·𝑜
z) ∈
𝜔 ∧ (y ·𝑜 w) ∈
N) ∧ ((x ·𝑜 v) ∈ 𝜔
∧ (y
·𝑜 u) ∈ N)) → ([〈(x ·𝑜 z), (y
·𝑜 w)〉]
~Q0 +Q0 [〈(x ·𝑜 v), (y
·𝑜 u)〉]
~Q0 ) = [〈(((x ·𝑜 z) ·𝑜 (y ·𝑜 u)) +𝑜 ((y ·𝑜 w) ·𝑜 (x ·𝑜 v))), ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))〉]
~Q0 ) |
147 | 139, 145,
146 | syl2an 273 |
. . . . . . . . . 10
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N)) ∧ ((x ∈ 𝜔 ∧
y ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N))) → ([〈(x ·𝑜 z), (y
·𝑜 w)〉]
~Q0 +Q0 [〈(x ·𝑜 v), (y
·𝑜 u)〉]
~Q0 ) = [〈(((x ·𝑜 z) ·𝑜 (y ·𝑜 u)) +𝑜 ((y ·𝑜 w) ·𝑜 (x ·𝑜 v))), ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))〉]
~Q0 ) |
148 | 133, 147 | eqtrd 2069 |
. . . . . . . . 9
⊢
((((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N)) ∧ ((x ∈ 𝜔 ∧
y ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N))) → (([〈x, y〉]
~Q0 ·Q0
[〈z, w〉] ~Q0 )
+Q0 ([〈x,
y〉] ~Q0
·Q0 [〈v, u〉]
~Q0 )) = [〈(((x ·𝑜 z) ·𝑜 (y ·𝑜 u)) +𝑜 ((y ·𝑜 w) ·𝑜 (x ·𝑜 v))), ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))〉]
~Q0 ) |
149 | 148 | 3impdi 1189 |
. . . . . . . 8
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → (([〈x,
y〉] ~Q0
·Q0 [〈z, w〉]
~Q0 ) +Q0 ([〈x, y〉]
~Q0 ·Q0
[〈v, u〉] ~Q0 )) =
[〈(((x ·𝑜
z) ·𝑜 (y ·𝑜 u)) +𝑜 ((y ·𝑜 w) ·𝑜 (x ·𝑜 v))), ((y
·𝑜 w)
·𝑜 (y
·𝑜 u))〉]
~Q0 ) |
150 | 101, 130,
149 | 3eqtr4d 2079 |
. . . . . . 7
⊢
(((x ∈ 𝜔 ∧
y ∈
N) ∧ (z ∈ 𝜔
∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → ([〈x,
y〉] ~Q0
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = (([〈x, y〉]
~Q0 ·Q0
[〈z, w〉] ~Q0 )
+Q0 ([〈x,
y〉] ~Q0
·Q0 [〈v, u〉]
~Q0 ))) |
151 | 150 | 3expib 1106 |
. . . . . 6
⊢
((x ∈ 𝜔 ∧
y ∈
N) → (((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → ([〈x, y〉]
~Q0 ·Q0
([〈z, w〉] ~Q0
+Q0 [〈v,
u〉] ~Q0 )) =
(([〈x, y〉] ~Q0
·Q0 [〈z, w〉]
~Q0 ) +Q0 ([〈x, y〉]
~Q0 ·Q0
[〈v, u〉] ~Q0
)))) |
152 | 1, 19, 151 | ecoptocl 6129 |
. . . . 5
⊢ (A ∈
Q0 → (((z
∈ 𝜔 ∧ w ∈ N) ∧ (v ∈ 𝜔 ∧
u ∈
N)) → (A
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = ((A
·Q0 [〈z, w〉]
~Q0 ) +Q0 (A ·Q0
[〈v, u〉] ~Q0
)))) |
153 | 152 | com12 27 |
. . . 4
⊢
(((z ∈ 𝜔 ∧
w ∈
N) ∧ (v ∈ 𝜔
∧ u ∈ N)) → (A ∈
Q0 → (A
·Q0 ([〈z, w〉]
~Q0 +Q0 [〈v, u〉]
~Q0 )) = ((A
·Q0 [〈z, w〉]
~Q0 ) +Q0 (A ·Q0
[〈v, u〉] ~Q0
)))) |
154 | 1, 7, 13, 153 | 2ecoptocl 6130 |
. . 3
⊢
((B ∈ Q0 ∧ 𝐶 ∈
Q0) → (A
∈ Q0 →
(A ·Q0
(B +Q0 𝐶)) = ((A ·Q0 B) +Q0 (A ·Q0 𝐶)))) |
155 | 154 | com12 27 |
. 2
⊢ (A ∈
Q0 → ((B
∈ Q0 ∧ 𝐶 ∈
Q0) → (A
·Q0 (B
+Q0 𝐶)) = ((A
·Q0 B)
+Q0 (A
·Q0 𝐶)))) |
156 | 155 | 3impib 1101 |
1
⊢
((A ∈ Q0 ∧ B ∈ Q0 ∧ 𝐶 ∈
Q0) → (A
·Q0 (B
+Q0 𝐶)) = ((A
·Q0 B)
+Q0 (A
·Q0 𝐶))) |