Step | Hyp | Ref
| Expression |
1 | | df-nq0 7424 |
. . . 4
โข
Q0 = ((ฯ ร N)
/ ~Q0 ) |
2 | | oveq1 5882 |
. . . . . . 7
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ) =
(๐ต
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)) |
3 | 2 | oveq2d 5891 |
. . . . . 6
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ (๐ด ยทQ0
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
(๐ด
ยทQ0 (๐ต +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0
))) |
4 | | oveq2 5883 |
. . . . . . 7
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ (๐ด ยทQ0
[โจ๐ง, ๐คโฉ]
~Q0 ) = (๐ด ยทQ0 ๐ต)) |
5 | 4 | oveq1d 5890 |
. . . . . 6
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ((๐ด ยทQ0
[โจ๐ง, ๐คโฉ]
~Q0 ) +Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
))) |
6 | 3, 5 | eqeq12d 2192 |
. . . . 5
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ((๐ด ยทQ0
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )) โ (๐ด ยทQ0 (๐ต +Q0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)))) |
7 | 6 | imbi2d 230 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ((๐ด โ Q0 โ
(๐ด
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 ))) โ (๐ด โ Q0 โ
(๐ด
ยทQ0 (๐ต +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 ๐ต) +Q0 (๐ด
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
))))) |
8 | | oveq2 5883 |
. . . . . . 7
โข
([โจ๐ฃ, ๐ขโฉ]
~Q0 = ๐ถ โ (๐ต +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ) =
(๐ต
+Q0 ๐ถ)) |
9 | 8 | oveq2d 5891 |
. . . . . 6
โข
([โจ๐ฃ, ๐ขโฉ]
~Q0 = ๐ถ โ (๐ด ยทQ0 (๐ต +Q0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )) = (๐ด ยทQ0 (๐ต +Q0
๐ถ))) |
10 | | oveq2 5883 |
. . . . . . 7
โข
([โจ๐ฃ, ๐ขโฉ]
~Q0 = ๐ถ โ (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 ) = (๐ด ยทQ0 ๐ถ)) |
11 | 10 | oveq2d 5891 |
. . . . . 6
โข
([โจ๐ฃ, ๐ขโฉ]
~Q0 = ๐ถ โ ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 ๐ต) +Q0 (๐ด
ยทQ0 ๐ถ))) |
12 | 9, 11 | eqeq12d 2192 |
. . . . 5
โข
([โจ๐ฃ, ๐ขโฉ]
~Q0 = ๐ถ โ ((๐ด ยทQ0 (๐ต +Q0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ))
โ (๐ด
ยทQ0 (๐ต +Q0 ๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 ๐ถ)))) |
13 | 12 | imbi2d 230 |
. . . 4
โข
([โจ๐ฃ, ๐ขโฉ]
~Q0 = ๐ถ โ ((๐ด โ Q0 โ
(๐ด
ยทQ0 (๐ต +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 ๐ต) +Q0 (๐ด
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )))
โ (๐ด โ
Q0 โ (๐ด ยทQ0 (๐ต +Q0
๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 ๐ถ))))) |
14 | | oveq1 5882 |
. . . . . . . 8
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
(๐ด
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0
))) |
15 | | oveq1 5882 |
. . . . . . . . 9
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
(๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
16 | | oveq1 5882 |
. . . . . . . . 9
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ) =
(๐ด
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)) |
17 | 15, 16 | oveq12d 5893 |
. . . . . . . 8
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 ))) |
18 | 14, 17 | eqeq12d 2192 |
. . . . . . 7
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
(([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ))
โ (๐ด
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )))) |
19 | 18 | imbi2d 230 |
. . . . . 6
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ((((๐ง โ ฯ โง ๐ค โ N) โง (๐ฃ โ ฯ โง ๐ข โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
(([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )))
โ (((๐ง โ ฯ
โง ๐ค โ
N) โง (๐ฃ
โ ฯ โง ๐ข
โ N)) โ (๐ด ยทQ0
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 ))))) |
20 | | an42 587 |
. . . . . . . . . . . 12
โข (((๐ง โ ฯ โง ๐ข โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ((๐ง โ ฯ
โง ๐ค โ
N) โง (๐ฃ
โ ฯ โง ๐ข
โ N))) |
21 | 20 | anbi2i 457 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
((๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ))) โ ((๐ฅ โ ฯ โง ๐ฆ โ N) โง ((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ
N)))) |
22 | | 3anass 982 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฅ
โ ฯ โง ๐ฆ
โ N) โง ((๐ง โ ฯ โง ๐ข โ N) โง (๐ค โ N โง
๐ฃ โ
ฯ)))) |
23 | | 3anass 982 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ ((๐ฅ โ ฯ โง ๐ฆ โ N) โง ((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ
N)))) |
24 | 21, 22, 23 | 3bitr4i 212 |
. . . . . . . . . 10
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฅ
โ ฯ โง ๐ฆ
โ N) โง (๐ง โ ฯ โง ๐ค โ N) โง (๐ฃ โ ฯ โง ๐ข โ
N))) |
25 | | pinn 7308 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ N โ
๐ฆ โ
ฯ) |
26 | | nnmcl 6482 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ ฯ โง ๐ฅ โ ฯ) โ (๐ฆ ยทo ๐ฅ) โ
ฯ) |
27 | 25, 26 | sylan 283 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ N โง
๐ฅ โ ฯ) โ
(๐ฆ ยทo
๐ฅ) โ
ฯ) |
28 | 27 | ancoms 268 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ฯ โง ๐ฆ โ N) โ
(๐ฆ ยทo
๐ฅ) โ
ฯ) |
29 | | pinn 7308 |
. . . . . . . . . . . . 13
โข (๐ข โ N โ
๐ข โ
ฯ) |
30 | | nnmcl 6482 |
. . . . . . . . . . . . 13
โข ((๐ง โ ฯ โง ๐ข โ ฯ) โ (๐ง ยทo ๐ข) โ
ฯ) |
31 | 29, 30 | sylan2 286 |
. . . . . . . . . . . 12
โข ((๐ง โ ฯ โง ๐ข โ N) โ
(๐ง ยทo
๐ข) โ
ฯ) |
32 | | pinn 7308 |
. . . . . . . . . . . . 13
โข (๐ค โ N โ
๐ค โ
ฯ) |
33 | | nnmcl 6482 |
. . . . . . . . . . . . 13
โข ((๐ค โ ฯ โง ๐ฃ โ ฯ) โ (๐ค ยทo ๐ฃ) โ
ฯ) |
34 | 32, 33 | sylan 283 |
. . . . . . . . . . . 12
โข ((๐ค โ N โง
๐ฃ โ ฯ) โ
(๐ค ยทo
๐ฃ) โ
ฯ) |
35 | | nndi 6487 |
. . . . . . . . . . . 12
โข (((๐ฆ ยทo ๐ฅ) โ ฯ โง (๐ง ยทo ๐ข) โ ฯ โง (๐ค ยทo ๐ฃ) โ ฯ) โ ((๐ฆ ยทo ๐ฅ) ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))) = (((๐ฆ ยทo ๐ฅ) ยทo (๐ง ยทo ๐ข)) +o ((๐ฆ ยทo ๐ฅ) ยทo (๐ค ยทo ๐ฃ)))) |
36 | 28, 31, 34, 35 | syl3an 1280 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฆ
ยทo ๐ฅ)
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))) =
(((๐ฆ ยทo
๐ฅ) ยทo
(๐ง ยทo
๐ข)) +o ((๐ฆ ยทo ๐ฅ) ยทo (๐ค ยทo ๐ฃ)))) |
37 | | simp1r 1022 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ๐ฆ
โ N) |
38 | | simp1l 1021 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ๐ฅ
โ ฯ) |
39 | 31 | 3ad2ant2 1019 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ง
ยทo ๐ข)
โ ฯ) |
40 | 34 | 3ad2ant3 1020 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ค
ยทo ๐ฃ)
โ ฯ) |
41 | | nnacl 6481 |
. . . . . . . . . . . . 13
โข (((๐ง ยทo ๐ข) โ ฯ โง (๐ค ยทo ๐ฃ) โ ฯ) โ ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)) โ
ฯ) |
42 | 39, 40, 41 | syl2anc 411 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))
โ ฯ) |
43 | | nnmass 6488 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ ฯ โง ๐ฅ โ ฯ โง ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ) โ
((๐ฆ ยทo
๐ฅ) ยทo
((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ))) = (๐ฆ ยทo (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))))) |
44 | 25, 43 | syl3an1 1271 |
. . . . . . . . . . . 12
โข ((๐ฆ โ N โง
๐ฅ โ ฯ โง
((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ) โ
((๐ฆ ยทo
๐ฅ) ยทo
((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ))) = (๐ฆ ยทo (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))))) |
45 | 37, 38, 42, 44 | syl3anc 1238 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฆ
ยทo ๐ฅ)
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))) =
(๐ฆ ยทo
(๐ฅ ยทo
((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ))))) |
46 | | nnmcom 6490 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ ฯ โง ๐ฆ โ ฯ) โ (๐ฅ ยทo ๐ฆ) = (๐ฆ ยทo ๐ฅ)) |
47 | 25, 46 | sylan2 286 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ ฯ โง ๐ฆ โ N) โ
(๐ฅ ยทo
๐ฆ) = (๐ฆ ยทo ๐ฅ)) |
48 | 47 | oveq1d 5890 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ ฯ โง ๐ฆ โ N) โ
((๐ฅ ยทo
๐ฆ) ยทo
(๐ง ยทo
๐ข)) = ((๐ฆ ยทo ๐ฅ) ยทo (๐ง ยทo ๐ข))) |
49 | 48 | adantr 276 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ((๐ฅ
ยทo ๐ฆ)
ยทo (๐ง
ยทo ๐ข)) =
((๐ฆ ยทo
๐ฅ) ยทo
(๐ง ยทo
๐ข))) |
50 | | simpll 527 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ๐ฅ โ
ฯ) |
51 | 25 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ๐ฆ โ
ฯ) |
52 | | simprl 529 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ๐ง โ
ฯ) |
53 | | nnmcom 6490 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ฯ โง ๐ โ ฯ) โ (๐ ยทo ๐) = (๐ ยทo ๐)) |
54 | 53 | adantl 277 |
. . . . . . . . . . . . . . 15
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โง (๐ โ ฯ
โง ๐ โ ฯ))
โ (๐
ยทo ๐) =
(๐ ยทo
๐)) |
55 | | nnmass 6488 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ฯ โง ๐ โ ฯ โง โ โ ฯ) โ ((๐ ยทo ๐) ยทo โ) = (๐ ยทo (๐ ยทo โ))) |
56 | 55 | adantl 277 |
. . . . . . . . . . . . . . 15
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โง (๐ โ ฯ
โง ๐ โ ฯ
โง โ โ ฯ))
โ ((๐
ยทo ๐)
ยทo โ) =
(๐ ยทo
(๐ ยทo
โ))) |
57 | | simprr 531 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ๐ข โ
N) |
58 | 57, 29 | syl 14 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ๐ข โ
ฯ) |
59 | | nnmcl 6482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ฯ โง ๐ โ ฯ) โ (๐ ยทo ๐) โ
ฯ) |
60 | 59 | adantl 277 |
. . . . . . . . . . . . . . 15
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โง (๐ โ ฯ
โง ๐ โ ฯ))
โ (๐
ยทo ๐)
โ ฯ) |
61 | 50, 51, 52, 54, 56, 58, 60 | caov4d 6059 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ((๐ฅ
ยทo ๐ฆ)
ยทo (๐ง
ยทo ๐ข)) =
((๐ฅ ยทo
๐ง) ยทo
(๐ฆ ยทo
๐ข))) |
62 | 49, 61 | eqtr3d 2212 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N))
โ ((๐ฆ
ยทo ๐ฅ)
ยทo (๐ง
ยทo ๐ข)) =
((๐ฅ ยทo
๐ง) ยทo
(๐ฆ ยทo
๐ข))) |
63 | 62 | 3adant3 1017 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฆ
ยทo ๐ฅ)
ยทo (๐ง
ยทo ๐ข)) =
((๐ฅ ยทo
๐ง) ยทo
(๐ฆ ยทo
๐ข))) |
64 | 25 | ad2antlr 489 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ๐ฆ โ
ฯ) |
65 | | simpll 527 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ๐ฅ โ
ฯ) |
66 | | simprl 529 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ๐ค โ
N) |
67 | 66, 32 | syl 14 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ๐ค โ
ฯ) |
68 | 53 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โง (๐ โ ฯ
โง ๐ โ ฯ))
โ (๐
ยทo ๐) =
(๐ ยทo
๐)) |
69 | 55 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โง (๐ โ ฯ
โง ๐ โ ฯ
โง โ โ ฯ))
โ ((๐
ยทo ๐)
ยทo โ) =
(๐ ยทo
(๐ ยทo
โ))) |
70 | | simprr 531 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ๐ฃ โ
ฯ) |
71 | 59 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โง (๐ โ ฯ
โง ๐ โ ฯ))
โ (๐
ยทo ๐)
โ ฯ) |
72 | 64, 65, 67, 68, 69, 70, 71 | caov4d 6059 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ((๐ฆ
ยทo ๐ฅ)
ยทo (๐ค
ยทo ๐ฃ)) =
((๐ฆ ยทo
๐ค) ยทo
(๐ฅ ยทo
๐ฃ))) |
73 | 72 | 3adant2 1016 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฆ
ยทo ๐ฅ)
ยทo (๐ค
ยทo ๐ฃ)) =
((๐ฆ ยทo
๐ค) ยทo
(๐ฅ ยทo
๐ฃ))) |
74 | 63, 73 | oveq12d 5893 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (((๐ฆ ยทo ๐ฅ) ยทo (๐ง ยทo ๐ข)) +o ((๐ฆ ยทo ๐ฅ) ยทo (๐ค ยทo ๐ฃ))) = (((๐ฅ ยทo ๐ง) ยทo (๐ฆ ยทo ๐ข)) +o ((๐ฆ ยทo ๐ค) ยทo (๐ฅ ยทo ๐ฃ)))) |
75 | 36, 45, 74 | 3eqtr3d 2218 |
. . . . . . . . . 10
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))))
= (((๐ฅ ยทo
๐ง) ยทo
(๐ฆ ยทo
๐ข)) +o ((๐ฆ ยทo ๐ค) ยทo (๐ฅ ยทo ๐ฃ)))) |
76 | 24, 75 | sylbir 135 |
. . . . . . . . 9
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ (๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))))
= (((๐ฅ ยทo
๐ง) ยทo
(๐ฆ ยทo
๐ข)) +o ((๐ฆ ยทo ๐ค) ยทo (๐ฅ ยทo ๐ฃ)))) |
77 | 37, 25 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ๐ฆ
โ ฯ) |
78 | | mulpiord 7316 |
. . . . . . . . . . . . . . . 16
โข ((๐ค โ N โง
๐ข โ N)
โ (๐ค
ยทN ๐ข) = (๐ค ยทo ๐ข)) |
79 | 78 | ancoms 268 |
. . . . . . . . . . . . . . 15
โข ((๐ข โ N โง
๐ค โ N)
โ (๐ค
ยทN ๐ข) = (๐ค ยทo ๐ข)) |
80 | 79 | ad2ant2lr 510 |
. . . . . . . . . . . . . 14
โข (((๐ง โ ฯ โง ๐ข โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ (๐ค
ยทN ๐ข) = (๐ค ยทo ๐ข)) |
81 | 80 | 3adant1 1015 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ค
ยทN ๐ข) = (๐ค ยทo ๐ข)) |
82 | 66 | 3adant2 1016 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ๐ค
โ N) |
83 | 57 | 3adant3 1017 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ๐ข
โ N) |
84 | | mulclpi 7327 |
. . . . . . . . . . . . . . 15
โข ((๐ค โ N โง
๐ข โ N)
โ (๐ค
ยทN ๐ข) โ N) |
85 | 82, 83, 84 | syl2anc 411 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ค
ยทN ๐ข) โ N) |
86 | | pinn 7308 |
. . . . . . . . . . . . . 14
โข ((๐ค
ยทN ๐ข) โ N โ (๐ค
ยทN ๐ข) โ ฯ) |
87 | 85, 86 | syl 14 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ค
ยทN ๐ข) โ ฯ) |
88 | 81, 87 | eqeltrrd 2255 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ค
ยทo ๐ข)
โ ฯ) |
89 | | nnmass 6488 |
. . . . . . . . . . . 12
โข ((๐ฆ โ ฯ โง ๐ฆ โ ฯ โง (๐ค ยทo ๐ข) โ ฯ) โ ((๐ฆ ยทo ๐ฆ) ยทo (๐ค ยทo ๐ข)) = (๐ฆ ยทo (๐ฆ ยทo (๐ค ยทo ๐ข)))) |
90 | 77, 77, 88, 89 | syl3anc 1238 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฆ
ยทo ๐ฆ)
ยทo (๐ค
ยทo ๐ข)) =
(๐ฆ ยทo
(๐ฆ ยทo
(๐ค ยทo
๐ข)))) |
91 | 82, 32 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ๐ค
โ ฯ) |
92 | 53 | adantl 277 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โง (๐
โ ฯ โง ๐
โ ฯ)) โ (๐
ยทo ๐) =
(๐ ยทo
๐)) |
93 | 55 | adantl 277 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โง (๐
โ ฯ โง ๐
โ ฯ โง โ
โ ฯ)) โ ((๐
ยทo ๐)
ยทo โ) =
(๐ ยทo
(๐ ยทo
โ))) |
94 | 83, 29 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ๐ข
โ ฯ) |
95 | 59 | adantl 277 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โง (๐
โ ฯ โง ๐
โ ฯ)) โ (๐
ยทo ๐)
โ ฯ) |
96 | 77, 77, 91, 92, 93, 94, 95 | caov4d 6059 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ ((๐ฆ
ยทo ๐ฆ)
ยทo (๐ค
ยทo ๐ข)) =
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))) |
97 | 90, 96 | eqtr3d 2212 |
. . . . . . . . . 10
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ ฯ)) โ (๐ฆ
ยทo (๐ฆ
ยทo (๐ค
ยทo ๐ข))) =
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))) |
98 | 24, 97 | sylbir 135 |
. . . . . . . . 9
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ (๐ฆ
ยทo (๐ฆ
ยทo (๐ค
ยทo ๐ข))) =
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))) |
99 | | opeq12 3781 |
. . . . . . . . . 10
โข (((๐ฆ ยทo (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)))) = (((๐ฅ ยทo ๐ง) ยทo (๐ฆ ยทo ๐ข)) +o ((๐ฆ ยทo ๐ค) ยทo (๐ฅ ยทo ๐ฃ))) โง (๐ฆ ยทo (๐ฆ ยทo (๐ค ยทo ๐ข))) = ((๐ฆ ยทo ๐ค) ยทo (๐ฆ ยทo ๐ข))) โ โจ(๐ฆ ยทo (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)))), (๐ฆ ยทo (๐ฆ ยทo (๐ค ยทo ๐ข)))โฉ = โจ(((๐ฅ ยทo ๐ง) ยทo (๐ฆ ยทo ๐ข)) +o ((๐ฆ ยทo ๐ค) ยทo (๐ฅ ยทo ๐ฃ))), ((๐ฆ ยทo ๐ค) ยทo (๐ฆ ยทo ๐ข))โฉ) |
100 | 99 | eceq1d 6571 |
. . . . . . . . 9
โข (((๐ฆ ยทo (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)))) = (((๐ฅ ยทo ๐ง) ยทo (๐ฆ ยทo ๐ข)) +o ((๐ฆ ยทo ๐ค) ยทo (๐ฅ ยทo ๐ฃ))) โง (๐ฆ ยทo (๐ฆ ยทo (๐ค ยทo ๐ข))) = ((๐ฆ ยทo ๐ค) ยทo (๐ฆ ยทo ๐ข))) โ [โจ(๐ฆ ยทo (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)))), (๐ฆ ยทo (๐ฆ ยทo (๐ค ยทo ๐ข)))โฉ] ~Q0 =
[โจ(((๐ฅ
ยทo ๐ง)
ยทo (๐ฆ
ยทo ๐ข))
+o ((๐ฆ
ยทo ๐ค)
ยทo (๐ฅ
ยทo ๐ฃ))),
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))โฉ]
~Q0 ) |
101 | 76, 98, 100 | syl2anc 411 |
. . . . . . . 8
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ [โจ(๐ฆ ยทo (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)))), (๐ฆ ยทo (๐ฆ ยทo (๐ค ยทo ๐ข)))โฉ] ~Q0 =
[โจ(((๐ฅ
ยทo ๐ง)
ยทo (๐ฆ
ยทo ๐ข))
+o ((๐ฆ
ยทo ๐ค)
ยทo (๐ฅ
ยทo ๐ฃ))),
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))โฉ]
~Q0 ) |
102 | | addnnnq0 7448 |
. . . . . . . . . . . 12
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ ([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ) =
[โจ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)),
(๐ค ยทo
๐ข)โฉ]
~Q0 ) |
103 | 102 | oveq2d 5891 |
. . . . . . . . . . 11
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)), (๐ค ยทo ๐ข)โฉ] ~Q0
)) |
104 | 103 | adantl 277 |
. . . . . . . . . 10
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
((๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N))) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)), (๐ค ยทo ๐ข)โฉ] ~Q0
)) |
105 | 31, 34, 41 | syl2an 289 |
. . . . . . . . . . . . 13
โข (((๐ง โ ฯ โง ๐ข โ N) โง
(๐ค โ N
โง ๐ฃ โ ฯ))
โ ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))
โ ฯ) |
106 | 105 | an42s 589 |
. . . . . . . . . . . 12
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))
โ ฯ) |
107 | 84 | ad2ant2l 508 |
. . . . . . . . . . . . 13
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ (๐ค
ยทN ๐ข) โ N) |
108 | 78 | eleq1d 2246 |
. . . . . . . . . . . . . 14
โข ((๐ค โ N โง
๐ข โ N)
โ ((๐ค
ยทN ๐ข) โ N โ (๐ค ยทo ๐ข) โ
N)) |
109 | 108 | ad2ant2l 508 |
. . . . . . . . . . . . 13
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ ((๐ค
ยทN ๐ข) โ N โ (๐ค ยทo ๐ข) โ
N)) |
110 | 107, 109 | mpbid 147 |
. . . . . . . . . . . 12
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ (๐ค
ยทo ๐ข)
โ N) |
111 | 106, 110 | jca 306 |
. . . . . . . . . . 11
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ (((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))
โ ฯ โง (๐ค
ยทo ๐ข)
โ N)) |
112 | | mulnnnq0 7449 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ โง (๐ค ยทo ๐ข) โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)), (๐ค ยทo ๐ข)โฉ] ~Q0 ) =
[โจ(๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ))),
(๐ฆ ยทo
(๐ค ยทo
๐ข))โฉ]
~Q0 ) |
113 | | nnmcl 6482 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ ฯ โง ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ) โ (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))) โ
ฯ) |
114 | | simpl 109 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ N โง
(๐ค ยทo
๐ข) โ N)
โ ๐ฆ โ
N) |
115 | | mulpiord 7316 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ N โง
(๐ค ยทo
๐ข) โ N)
โ (๐ฆ
ยทN (๐ค ยทo ๐ข)) = (๐ฆ ยทo (๐ค ยทo ๐ข))) |
116 | | mulclpi 7327 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ N โง
(๐ค ยทo
๐ข) โ N)
โ (๐ฆ
ยทN (๐ค ยทo ๐ข)) โ N) |
117 | 115, 116 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ N โง
(๐ค ยทo
๐ข) โ N)
โ (๐ฆ
ยทo (๐ค
ยทo ๐ข))
โ N) |
118 | 114, 117 | jca 306 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ N โง
(๐ค ยทo
๐ข) โ N)
โ (๐ฆ โ
N โง (๐ฆ
ยทo (๐ค
ยทo ๐ข))
โ N)) |
119 | 113, 118 | anim12i 338 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ฯ โง ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ) โง (๐ฆ โ N โง
(๐ค ยทo
๐ข) โ N))
โ ((๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))
โ ฯ โง (๐ฆ
โ N โง (๐ฆ ยทo (๐ค ยทo ๐ข)) โ N))) |
120 | | an12 561 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))) โ ฯ โง (๐ฆ โ N โง
(๐ฆ ยทo
(๐ค ยทo
๐ข)) โ
N)) โ (๐ฆ
โ N โง ((๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))) โ ฯ โง (๐ฆ ยทo (๐ค ยทo ๐ข)) โ N))) |
121 | | 3anass 982 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ N โง
(๐ฅ ยทo
((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ))) โ ฯ โง (๐ฆ ยทo (๐ค ยทo ๐ข)) โ N)
โ (๐ฆ โ
N โง ((๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))
โ ฯ โง (๐ฆ
ยทo (๐ค
ยทo ๐ข))
โ N))) |
122 | 120, 121 | bitr4i 187 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))) โ ฯ โง (๐ฆ โ N โง
(๐ฆ ยทo
(๐ค ยทo
๐ข)) โ
N)) โ (๐ฆ
โ N โง (๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))) โ ฯ โง (๐ฆ ยทo (๐ค ยทo ๐ข)) โ N)) |
123 | 119, 122 | sylib 122 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ ฯ โง ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ) โง (๐ฆ โ N โง
(๐ค ยทo
๐ข) โ N))
โ (๐ฆ โ
N โง (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))
โ ฯ โง (๐ฆ
ยทo (๐ค
ยทo ๐ข))
โ N)) |
124 | 123 | an4s 588 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ โง (๐ค ยทo ๐ข) โ N))
โ (๐ฆ โ
N โง (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))
โ ฯ โง (๐ฆ
ยทo (๐ค
ยทo ๐ข))
โ N)) |
125 | | mulcanenq0ec 7444 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ N โง
(๐ฅ ยทo
((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ))) โ ฯ โง (๐ฆ ยทo (๐ค ยทo ๐ข)) โ N)
โ [โจ(๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))),
(๐ฆ ยทo
(๐ฆ ยทo
(๐ค ยทo
๐ข)))โฉ]
~Q0 = [โจ(๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))), (๐ฆ ยทo (๐ค ยทo ๐ข))โฉ] ~Q0
) |
126 | 124, 125 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ โง (๐ค ยทo ๐ข) โ N))
โ [โจ(๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))),
(๐ฆ ยทo
(๐ฆ ยทo
(๐ค ยทo
๐ข)))โฉ]
~Q0 = [โจ(๐ฅ ยทo ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ))), (๐ฆ ยทo (๐ค ยทo ๐ข))โฉ] ~Q0
) |
127 | 112, 126 | eqtr4d 2213 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(((๐ง ยทo
๐ข) +o (๐ค ยทo ๐ฃ)) โ ฯ โง (๐ค ยทo ๐ข) โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)), (๐ค ยทo ๐ข)โฉ] ~Q0 ) =
[โจ(๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))),
(๐ฆ ยทo
(๐ฆ ยทo
(๐ค ยทo
๐ข)))โฉ]
~Q0 ) |
128 | 111, 127 | sylan2 286 |
. . . . . . . . . 10
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
((๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N))) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ((๐ง ยทo ๐ข) +o (๐ค ยทo ๐ฃ)), (๐ค ยทo ๐ข)โฉ] ~Q0 ) =
[โจ(๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))),
(๐ฆ ยทo
(๐ฆ ยทo
(๐ค ยทo
๐ข)))โฉ]
~Q0 ) |
129 | 104, 128 | eqtrd 2210 |
. . . . . . . . 9
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
((๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N))) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
[โจ(๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))),
(๐ฆ ยทo
(๐ฆ ยทo
(๐ค ยทo
๐ข)))โฉ]
~Q0 ) |
130 | 129 | 3impb 1199 |
. . . . . . . 8
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
[โจ(๐ฆ
ยทo (๐ฅ
ยทo ((๐ง
ยทo ๐ข)
+o (๐ค
ยทo ๐ฃ)))),
(๐ฆ ยทo
(๐ฆ ยทo
(๐ค ยทo
๐ข)))โฉ]
~Q0 ) |
131 | | mulnnnq0 7449 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
[โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 ) |
132 | | mulnnnq0 7449 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ) =
[โจ(๐ฅ
ยทo ๐ฃ),
(๐ฆ ยทo
๐ข)โฉ]
~Q0 ) |
133 | 131, 132 | oveqan12d 5894 |
. . . . . . . . . 10
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โง ((๐ฅ โ ฯ
โง ๐ฆ โ
N) โง (๐ฃ
โ ฯ โง ๐ข
โ N))) โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
([โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 +Q0 [โจ(๐ฅ ยทo ๐ฃ), (๐ฆ ยทo ๐ข)โฉ] ~Q0
)) |
134 | | nnmcl 6482 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ ฯ โง ๐ง โ ฯ) โ (๐ฅ ยทo ๐ง) โ
ฯ) |
135 | | mulpiord 7316 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) = (๐ฆ ยทo ๐ค)) |
136 | | mulclpi 7327 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) โ N) |
137 | 135, 136 | eqeltrrd 2255 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทo ๐ค)
โ N) |
138 | 134, 137 | anim12i 338 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ง โ ฯ) โง (๐ฆ โ N โง
๐ค โ N))
โ ((๐ฅ
ยทo ๐ง)
โ ฯ โง (๐ฆ
ยทo ๐ค)
โ N)) |
139 | 138 | an4s 588 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ((๐ฅ
ยทo ๐ง)
โ ฯ โง (๐ฆ
ยทo ๐ค)
โ N)) |
140 | | nnmcl 6482 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ ฯ โง ๐ฃ โ ฯ) โ (๐ฅ ยทo ๐ฃ) โ
ฯ) |
141 | | mulpiord 7316 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ N โง
๐ข โ N)
โ (๐ฆ
ยทN ๐ข) = (๐ฆ ยทo ๐ข)) |
142 | | mulclpi 7327 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ N โง
๐ข โ N)
โ (๐ฆ
ยทN ๐ข) โ N) |
143 | 141, 142 | eqeltrrd 2255 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ N โง
๐ข โ N)
โ (๐ฆ
ยทo ๐ข)
โ N) |
144 | 140, 143 | anim12i 338 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ฯ โง ๐ฃ โ ฯ) โง (๐ฆ โ N โง
๐ข โ N))
โ ((๐ฅ
ยทo ๐ฃ)
โ ฯ โง (๐ฆ
ยทo ๐ข)
โ N)) |
145 | 144 | an4s 588 |
. . . . . . . . . . 11
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ ((๐ฅ
ยทo ๐ฃ)
โ ฯ โง (๐ฆ
ยทo ๐ข)
โ N)) |
146 | | addnnnq0 7448 |
. . . . . . . . . . 11
โข ((((๐ฅ ยทo ๐ง) โ ฯ โง (๐ฆ ยทo ๐ค) โ N) โง
((๐ฅ ยทo
๐ฃ) โ ฯ โง
(๐ฆ ยทo
๐ข) โ N))
โ ([โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 +Q0 [โจ(๐ฅ ยทo ๐ฃ), (๐ฆ ยทo ๐ข)โฉ] ~Q0 ) =
[โจ(((๐ฅ
ยทo ๐ง)
ยทo (๐ฆ
ยทo ๐ข))
+o ((๐ฆ
ยทo ๐ค)
ยทo (๐ฅ
ยทo ๐ฃ))),
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))โฉ]
~Q0 ) |
147 | 139, 145,
146 | syl2an 289 |
. . . . . . . . . 10
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โง ((๐ฅ โ ฯ
โง ๐ฆ โ
N) โง (๐ฃ
โ ฯ โง ๐ข
โ N))) โ ([โจ(๐ฅ ยทo ๐ง), (๐ฆ ยทo ๐ค)โฉ] ~Q0
+Q0 [โจ(๐ฅ ยทo ๐ฃ), (๐ฆ ยทo ๐ข)โฉ] ~Q0 ) =
[โจ(((๐ฅ
ยทo ๐ง)
ยทo (๐ฆ
ยทo ๐ข))
+o ((๐ฆ
ยทo ๐ค)
ยทo (๐ฅ
ยทo ๐ฃ))),
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))โฉ]
~Q0 ) |
148 | 133, 147 | eqtrd 2210 |
. . . . . . . . 9
โข ((((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โง ((๐ฅ โ ฯ
โง ๐ฆ โ
N) โง (๐ฃ
โ ฯ โง ๐ข
โ N))) โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
[โจ(((๐ฅ
ยทo ๐ง)
ยทo (๐ฆ
ยทo ๐ข))
+o ((๐ฆ
ยทo ๐ค)
ยทo (๐ฅ
ยทo ๐ฃ))),
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))โฉ]
~Q0 ) |
149 | 148 | 3impdi 1293 |
. . . . . . . 8
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
[โจ(((๐ฅ
ยทo ๐ง)
ยทo (๐ฆ
ยทo ๐ข))
+o ((๐ฆ
ยทo ๐ค)
ยทo (๐ฅ
ยทo ๐ฃ))),
((๐ฆ ยทo
๐ค) ยทo
(๐ฆ ยทo
๐ข))โฉ]
~Q0 ) |
150 | 101, 130,
149 | 3eqtr4d 2220 |
. . . . . . 7
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
(([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
))) |
151 | 150 | 3expib 1206 |
. . . . . 6
โข ((๐ฅ โ ฯ โง ๐ฆ โ N) โ
(((๐ง โ ฯ โง
๐ค โ N)
โง (๐ฃ โ ฯ
โง ๐ข โ
N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
(([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)))) |
152 | 1, 19, 151 | ecoptocl 6622 |
. . . . 5
โข (๐ด โ
Q0 โ (((๐ง โ ฯ โง ๐ค โ N) โง (๐ฃ โ ฯ โง ๐ข โ N)) โ
(๐ด
ยทQ0 ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )))) |
153 | 152 | com12 30 |
. . . 4
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ (๐ด โ
Q0 โ (๐ด ยทQ0
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ฃ, ๐ขโฉ] ~Q0 )) =
((๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 )
+Q0 (๐ด ยทQ0
[โจ๐ฃ, ๐ขโฉ]
~Q0 )))) |
154 | 1, 7, 13, 153 | 2ecoptocl 6623 |
. . 3
โข ((๐ต โ
Q0 โง ๐ถ โ Q0) โ
(๐ด โ
Q0 โ (๐ด ยทQ0 (๐ต +Q0
๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 ๐ถ)))) |
155 | 154 | com12 30 |
. 2
โข (๐ด โ
Q0 โ ((๐ต โ Q0 โง
๐ถ โ
Q0) โ (๐ด ยทQ0 (๐ต +Q0
๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 ๐ถ)))) |
156 | 155 | 3impib 1201 |
1
โข ((๐ด โ
Q0 โง ๐ต โ Q0 โง
๐ถ โ
Q0) โ (๐ด ยทQ0 (๐ต +Q0
๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0
(๐ด
ยทQ0 ๐ถ))) |