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
๐ท)โฉ]
~Q0 = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ]
~Q0 |
13 | | opeq12 3782 |
. . . . . 6
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ) |
14 | | eceq1 6572 |
. . . . . . . . 9
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ [โจ๐ค, ๐ฃโฉ] ~Q0 =
[โจ๐ด, ๐ตโฉ] ~Q0
) |
15 | 14 | eqeq2d 2189 |
. . . . . . . 8
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ ([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โ [โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ด, ๐ตโฉ] ~Q0
)) |
16 | 15 | anbi1d 465 |
. . . . . . 7
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ (([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 )
โ ([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
))) |
17 | | vex 2742 |
. . . . . . . . . . 11
โข ๐ค โ V |
18 | | vex 2742 |
. . . . . . . . . . 11
โข ๐ฃ โ V |
19 | 17, 18 | opth 4239 |
. . . . . . . . . 10
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ (๐ค = ๐ด โง ๐ฃ = ๐ต)) |
20 | | oveq1 5884 |
. . . . . . . . . . . 12
โข (๐ค = ๐ด โ (๐ค ยทo ๐ถ) = (๐ด ยทo ๐ถ)) |
21 | 20 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ (๐ค ยทo ๐ถ) = (๐ด ยทo ๐ถ)) |
22 | | oveq1 5884 |
. . . . . . . . . . . 12
โข (๐ฃ = ๐ต โ (๐ฃ ยทo ๐ท) = (๐ต ยทo ๐ท)) |
23 | 22 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ (๐ฃ ยทo ๐ท) = (๐ต ยทo ๐ท)) |
24 | 21, 23 | opeq12d 3788 |
. . . . . . . . . 10
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ = โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ) |
25 | 19, 24 | sylbi 121 |
. . . . . . . . 9
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ = โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ) |
26 | 25 | eceq1d 6573 |
. . . . . . . 8
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 ) |
27 | 26 | eqeq2d 2189 |
. . . . . . 7
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ ([โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ถ),
(๐ฃ ยทo
๐ท)โฉ]
~Q0 โ [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 )) |
28 | 16, 27 | anbi12d 473 |
. . . . . 6
โข
(โจ๐ค, ๐ฃโฉ = โจ๐ด, ๐ตโฉ โ ((([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0 )
โ (([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0
))) |
29 | 13, 28 | syl 14 |
. . . . 5
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ((([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0 )
โ (([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0
))) |
30 | 29 | spc2egv 2829 |
. . . 4
โข ((๐ด โ ฯ โง ๐ต โ N) โ
((([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ โ๐คโ๐ฃ(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0
))) |
31 | | opeq12 3782 |
. . . . . . 7
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ) |
32 | | eceq1 6572 |
. . . . . . . . . 10
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ [โจ๐ข, ๐กโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
) |
33 | 32 | eqeq2d 2189 |
. . . . . . . . 9
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ ([โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 โ [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
)) |
34 | 33 | anbi2d 464 |
. . . . . . . 8
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ (([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โ ([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0
))) |
35 | | vex 2742 |
. . . . . . . . . . . 12
โข ๐ข โ V |
36 | | vex 2742 |
. . . . . . . . . . . 12
โข ๐ก โ V |
37 | 35, 36 | opth 4239 |
. . . . . . . . . . 11
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ (๐ข = ๐ถ โง ๐ก = ๐ท)) |
38 | | oveq2 5885 |
. . . . . . . . . . . . 13
โข (๐ข = ๐ถ โ (๐ค ยทo ๐ข) = (๐ค ยทo ๐ถ)) |
39 | 38 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ (๐ค ยทo ๐ข) = (๐ค ยทo ๐ถ)) |
40 | | oveq2 5885 |
. . . . . . . . . . . . 13
โข (๐ก = ๐ท โ (๐ฃ ยทo ๐ก) = (๐ฃ ยทo ๐ท)) |
41 | 40 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ (๐ฃ ยทo ๐ก) = (๐ฃ ยทo ๐ท)) |
42 | 39, 41 | opeq12d 3788 |
. . . . . . . . . . 11
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ = โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ) |
43 | 37, 42 | sylbi 121 |
. . . . . . . . . 10
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ = โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ) |
44 | 43 | eceq1d 6573 |
. . . . . . . . 9
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ถ),
(๐ฃ ยทo
๐ท)โฉ]
~Q0 ) |
45 | 44 | eqeq2d 2189 |
. . . . . . . 8
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ ([โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 โ [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ถ),
(๐ฃ ยทo
๐ท)โฉ]
~Q0 )) |
46 | 34, 45 | anbi12d 473 |
. . . . . . 7
โข
(โจ๐ข, ๐กโฉ = โจ๐ถ, ๐ทโฉ โ ((([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ) โ (([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0
))) |
47 | 31, 46 | syl 14 |
. . . . . 6
โข ((๐ข = ๐ถ โง ๐ก = ๐ท) โ ((([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ) โ (([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0
))) |
48 | 47 | spc2egv 2829 |
. . . . 5
โข ((๐ถ โ ฯ โง ๐ท โ N) โ
((([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0 )
โ โ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
49 | 48 | 2eximdv 1882 |
. . . 4
โข ((๐ถ โ ฯ โง ๐ท โ N) โ
(โ๐คโ๐ฃ(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ถ), (๐ฃ ยทo ๐ท)โฉ] ~Q0 )
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
50 | 30, 49 | sylan9 409 |
. . 3
โข (((๐ด โ ฯ โง ๐ต โ N) โง
(๐ถ โ ฯ โง
๐ท โ N))
โ ((([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ด, ๐ตโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
51 | 11, 12, 50 | mp2ani 432 |
. 2
โข (((๐ด โ ฯ โง ๐ต โ N) โง
(๐ถ โ ฯ โง
๐ท โ N))
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 )) |
52 | | ecexg 6541 |
. . . 4
โข (
~Q0 โ V โ [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 โ
V) |
53 | 2, 52 | ax-mp 5 |
. . 3
โข
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 โ V |
54 | | eqeq1 2184 |
. . . . . . . 8
โข (๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โ
(๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โ
[โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 )) |
55 | | eqeq1 2184 |
. . . . . . . 8
โข (๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โ
(๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 โ
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 )) |
56 | 54, 55 | bi2anan9 606 |
. . . . . . 7
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 )
โ ((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โ
([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ))) |
57 | | eqeq1 2184 |
. . . . . . 7
โข (๐ง = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 โ
(๐ง = [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0 โ
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 = [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0
)) |
58 | 56, 57 | bi2anan9 606 |
. . . . . 6
โข (((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 ) โง
๐ง = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0 )
โ (([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
59 | 58 | 3impa 1194 |
. . . . 5
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0 )
โ (([โจ๐ด, ๐ตโฉ]
~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
[โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
60 | 59 | 4exbidv 1870 |
. . . 4
โข ((๐ฅ = [โจ๐ด, ๐ตโฉ] ~Q0 โง
๐ฆ = [โจ๐ถ, ๐ทโฉ] ~Q0 โง
๐ง = [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 )
โ (โ๐คโ๐ฃโ๐ขโ๐ก((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0 )
โ โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ))) |
61 | | mulnq0mo 7449 |
. . . 4
โข ((๐ฅ โ ((ฯ ร
N) / ~Q0 ) โง ๐ฆ โ ((ฯ ร
N) / ~Q0 )) โ โ*๐งโ๐คโ๐ฃโ๐ขโ๐ก((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0
)) |
62 | | dfmq0qs 7430 |
. . . 4
โข
ยทQ0 = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ((ฯ ร N)
/ ~Q0 ) โง ๐ฆ โ ((ฯ ร N)
/ ~Q0 )) โง โ๐คโ๐ฃโ๐ขโ๐ก((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
๐ฆ = [โจ๐ข, ๐กโฉ] ~Q0 ) โง
๐ง = [โจ(๐ค ยทo ๐ข), (๐ฃ ยทo ๐ก)โฉ] ~Q0
))} |
63 | 60, 61, 62 | ovig 5998 |
. . 3
โข
(([โจ๐ด, ๐ตโฉ]
~Q0 โ ((ฯ ร N) /
~Q0 ) โง [โจ๐ถ, ๐ทโฉ] ~Q0 โ
((ฯ ร N) / ~Q0 )
โง [โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 โ V) โ (โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ) โ ([โจ๐ด, ๐ตโฉ] ~Q0
ยทQ0 [โจ๐ถ, ๐ทโฉ] ~Q0 ) =
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 )) |
64 | 53, 63 | mp3an3 1326 |
. 2
โข
(([โจ๐ด, ๐ตโฉ]
~Q0 โ ((ฯ ร N) /
~Q0 ) โง [โจ๐ถ, ๐ทโฉ] ~Q0 โ
((ฯ ร N) / ~Q0 ))
โ (โ๐คโ๐ฃโ๐ขโ๐ก(([โจ๐ด, ๐ตโฉ] ~Q0 =
[โจ๐ค, ๐ฃโฉ]
~Q0 โง [โจ๐ถ, ๐ทโฉ] ~Q0 =
[โจ๐ข, ๐กโฉ]
~Q0 ) โง [โจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โฉ] ~Q0 =
[โจ(๐ค
ยทo ๐ข),
(๐ฃ ยทo
๐ก)โฉ]
~Q0 ) โ ([โจ๐ด, ๐ตโฉ] ~Q0
ยทQ0 [โจ๐ถ, ๐ทโฉ] ~Q0 ) =
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 )) |
65 | 8, 51, 64 | sylc 62 |
1
โข (((๐ด โ ฯ โง ๐ต โ N) โง
(๐ถ โ ฯ โง
๐ท โ N))
โ ([โจ๐ด, ๐ตโฉ]
~Q0 ยทQ0 [โจ๐ถ, ๐ทโฉ] ~Q0 ) =
[โจ(๐ด
ยทo ๐ถ),
(๐ต ยทo
๐ท)โฉ]
~Q0 ) |