Step | Hyp | Ref
| Expression |
1 | | opelxpi 4660 |
. . . 4
โข ((๐ด โ ฯ โง ๐ต โ N) โ
โจ๐ด, ๐ตโฉ โ (ฯ ร
N)) |
2 | | enq0ex 7440 |
. . . . 5
โข
~Q0 โ V |
3 | 2 | ecelqsi 6591 |
. . . 4
โข
(โจ๐ด, ๐ตโฉ โ (ฯ ร
N) โ [โจ๐ด, ๐ตโฉ] ~Q0 โ
((ฯ ร N) / ~Q0
)) |
4 | 1, 3 | syl 14 |
. . 3
โข ((๐ด โ ฯ โง ๐ต โ N) โ
[โจ๐ด, ๐ตโฉ] ~Q0 โ
((ฯ ร N) / ~Q0
)) |
5 | | opelxpi 4660 |
. . . 4
โข ((๐ถ โ ฯ โง ๐ท โ N) โ
โจ๐ถ, ๐ทโฉ โ (ฯ ร
N)) |
6 | 2 | ecelqsi 6591 |
. . . 4
โข
(โจ๐ถ, ๐ทโฉ โ (ฯ ร
N) โ [โจ๐ถ, ๐ทโฉ] ~Q0 โ
((ฯ ร N) / ~Q0
)) |
7 | 5, 6 | syl 14 |
. . 3
โข ((๐ถ โ ฯ โง ๐ท โ N) โ
[โจ๐ถ, ๐ทโฉ] ~Q0 โ
((ฯ ร N) / ~Q0
)) |
8 | 4, 7 | anim12i 338 |
. 2
โข (((๐ด โ ฯ โง ๐ต โ N) โง
(๐ถ โ ฯ โง
๐ท โ N))
โ ([โจ๐ด, ๐ตโฉ]
~Q0 โ ((ฯ ร N) /
~Q0 ) โง [โจ๐ถ, ๐ทโฉ] ~Q0 โ
((ฯ ร N) / ~Q0
))) |
9 | | eqid 2177 |
. . . 4
โข
[โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ]
~Q0 |
10 | | eqid 2177 |
. . . 4
โข
[โจ๐ถ, ๐ทโฉ]
~Q0 = [โจ๐ถ, ๐ทโฉ]
~Q0 |
11 | 9, 10 | pm3.2i 272 |
. . 3
โข
([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
) |
12 | | eqid 2177 |
. . 3
โข
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ]
~Q0 |
13 | | opeq12 3782 |
. . . . . . . . 9
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ) |
14 | 13 | eceq1d 6573 |
. . . . . . . 8
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ [โจ๐ค, ๐ฃโฉ] ~Q0 =
[โจ๐ด, ๐ตโฉ] ~Q0
) |
15 | 14 | eqeq2d 2189 |
. . . . . . 7
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โ [โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ด, ๐ตโฉ] ~Q0
)) |
16 | 15 | anbi1d 465 |
. . . . . 6
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ (([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 )
โ ([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
))) |
17 | | simpl 109 |
. . . . . . . . . . 11
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ๐ค = ๐ด) |
18 | 17 | oveq1d 5892 |
. . . . . . . . . 10
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ (๐ค ยทo ๐ท) = (๐ด ยทo ๐ท)) |
19 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ๐ฃ = ๐ต) |
20 | 19 | oveq1d 5892 |
. . . . . . . . . 10
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ (๐ฃ ยทo ๐ถ) = (๐ต ยทo ๐ถ)) |
21 | 18, 20 | oveq12d 5895 |
. . . . . . . . 9
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)) = ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ))) |
22 | 19 | oveq1d 5892 |
. . . . . . . . 9
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ (๐ฃ ยทo ๐ท) = (๐ต ยทo ๐ท)) |
23 | 21, 22 | opeq12d 3788 |
. . . . . . . 8
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ = โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ) |
24 | 23 | eceq1d 6573 |
. . . . . . 7
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ [โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 ) |
25 | 24 | eqeq2d 2189 |
. . . . . 6
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ([โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ท)
+o (๐ฃ
ยทo ๐ถ)),
(๐ฃ ยทo
๐ท)โฉ]
~Q0 โ [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 )) |
26 | 16, 25 | anbi12d 473 |
. . . . 5
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ((([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ] ~Q0 )
โ (([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0
))) |
27 | 26 | spc2egv 2829 |
. . . 4
โข ((๐ด โ ฯ โง ๐ต โ N) โ
((([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ โ๐คโ๐ฃ(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ] ~Q0
))) |
28 | | opeq12 3782 |
. . . . . . . . . 10
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ) |
29 | 28 | eceq1d 6573 |
. . . . . . . . 9
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ [โจ๐ข, ๐กโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
) |
30 | 29 | eqeq2d 2189 |
. . . . . . . 8
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ ([โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 โ [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
)) |
31 | 30 | anbi2d 464 |
. . . . . . 7
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ (([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โ ([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
))) |
32 | | simpr 110 |
. . . . . . . . . . . 12
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ ๐ก = ๐ท) |
33 | 32 | oveq2d 5893 |
. . . . . . . . . . 11
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ (๐ค ยทo ๐ก) = (๐ค ยทo ๐ท)) |
34 | | simpl 109 |
. . . . . . . . . . . 12
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ ๐ข = ๐ถ) |
35 | 34 | oveq2d 5893 |
. . . . . . . . . . 11
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ (๐ฃ ยทo ๐ข) = (๐ฃ ยทo ๐ถ)) |
36 | 33, 35 | oveq12d 5895 |
. . . . . . . . . 10
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)) = ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ))) |
37 | 32 | oveq2d 5893 |
. . . . . . . . . 10
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ (๐ฃ ยทo ๐ก) = (๐ฃ ยทo ๐ท)) |
38 | 36, 37 | opeq12d 3788 |
. . . . . . . . 9
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ = โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ) |
39 | 38 | eceq1d 6573 |
. . . . . . . 8
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ [โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ท)
+o (๐ฃ
ยทo ๐ถ)),
(๐ฃ ยทo
๐ท)โฉ]
~Q0 ) |
40 | 39 | eqeq2d 2189 |
. . . . . . 7
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ ([โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 โ [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ท)
+o (๐ฃ
ยทo ๐ถ)),
(๐ฃ ยทo
๐ท)โฉ]
~Q0 )) |
41 | 31, 40 | anbi12d 473 |
. . . . . 6
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ ((([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ) โ (([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ] ~Q0
))) |
42 | 41 | spc2egv 2829 |
. . . . 5
โข ((๐ถ โ ฯ โง ๐ท โ N) โ
((([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ] ~Q0 )
โ โ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
43 | 42 | 2eximdv 1882 |
. . . 4
โข ((๐ถ โ ฯ โง ๐ท โ N) โ
(โ๐คโ๐ฃ(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ค ยทo ๐ท) +o (๐ฃ ยทo ๐ถ)), (๐ฃ ยทo ๐ท)โฉ] ~Q0 )
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
44 | 27, 43 | sylan9 409 |
. . 3
โข (((๐ด โ ฯ โง ๐ต โ N) โง
(๐ถ โ ฯ โง
๐ท โ N))
โ ((([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
45 | 11, 12, 44 | mp2ani 432 |
. 2
โข (((๐ด โ ฯ โง ๐ต โ N) โง
(๐ถ โ ฯ โง
๐ท โ N))
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 )) |
46 | | ecexg 6541 |
. . . 4
โข (
~Q0 โ V โ [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 โ
V) |
47 | 2, 46 | ax-mp 5 |
. . 3
โข
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 โ V |
48 | | simp1 997 |
. . . . . . . 8
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ ๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0
) |
49 | 48 | eqeq1d 2186 |
. . . . . . 7
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โ
[โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 )) |
50 | | simp2 998 |
. . . . . . . 8
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ ๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0
) |
51 | 50 | eqeq1d 2186 |
. . . . . . 7
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 โ
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 )) |
52 | 49, 51 | anbi12d 473 |
. . . . . 6
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ ((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โ
([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ))) |
53 | | simp3 999 |
. . . . . . 7
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ ๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0
) |
54 | 53 | eqeq1d 2186 |
. . . . . 6
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (๐ง = [โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ] ~Q0 โ
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ] ~Q0
)) |
55 | 52, 54 | anbi12d 473 |
. . . . 5
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ] ~Q0 )
โ (([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
56 | 55 | 4exbidv 1870 |
. . . 4
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (โ๐คโ๐ฃโ๐ขโ๐ก((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ] ~Q0 )
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
57 | | addnq0mo 7448 |
. . . 4
โข ((๐ฅ โ ((ฯ ร
N) / ~Q0 ) โง ๐ฆ โ ((ฯ ร
N) / ~Q0 )) โ โ*๐งโ๐คโ๐ฃโ๐ขโ๐ก((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ] ~Q0
)) |
58 | | dfplq0qs 7431 |
. . . 4
โข
+Q0 = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ((ฯ ร N)
/ ~Q0 ) โง ๐ฆ โ ((ฯ ร N)
/ ~Q0 )) โง โ๐คโ๐ฃโ๐ขโ๐ก((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ((๐ค ยทo ๐ก) +o (๐ฃ ยทo ๐ข)), (๐ฃ ยทo ๐ก)โฉ] ~Q0
))} |
59 | 56, 57, 58 | ovig 5998 |
. . 3
โข
(([โจ๐ด, ๐ตโฉ]
~Q0 โ ((ฯ ร N) /
~Q0 ) โง [โจ๐ถ, ๐ทโฉ] ~Q0 โ
((ฯ ร N) / ~Q0 )
โง [โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 โ V) โ (โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ) โ ([โจ๐ด, ๐ตโฉ] ~Q0
+Q0 [โจ๐ถ, ๐ทโฉ] ~Q0 ) =
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 )) |
60 | 47, 59 | mp3an3 1326 |
. 2
โข
(([โจ๐ด, ๐ตโฉ]
~Q0 โ ((ฯ ร N) /
~Q0 ) โง [โจ๐ถ, ๐ทโฉ] ~Q0 โ
((ฯ ร N) / ~Q0 ))
โ (โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ((๐ค
ยทo ๐ก)
+o (๐ฃ
ยทo ๐ข)),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ) โ ([โจ๐ด, ๐ตโฉ] ~Q0
+Q0 [โจ๐ถ, ๐ทโฉ] ~Q0 ) =
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 )) |
61 | 8, 45, 60 | sylc 62 |
1
โข (((๐ด โ ฯ โง ๐ต โ N) โง
(๐ถ โ ฯ โง
๐ท โ N))
โ ([โจ๐ด, ๐ตโฉ]
~Q0 +Q0 [โจ๐ถ, ๐ทโฉ] ~Q0 ) =
[โจ((๐ด
ยทo ๐ท)
+o (๐ต
ยทo ๐ถ)),
(๐ต ยทo
๐ท)โฉ]
~Q0 ) |