Step | Hyp | Ref
| Expression |
1 | | mulclpi 7326 |
. . . 4
โข ((๐ด โ N โง
๐ถ โ N)
โ (๐ด
ยทN ๐ถ) โ N) |
2 | | mulclpi 7326 |
. . . 4
โข ((๐ต โ N โง
๐ท โ N)
โ (๐ต
ยทN ๐ท) โ N) |
3 | | opelxpi 4658 |
. . . 4
โข (((๐ด
ยทN ๐ถ) โ N โง (๐ต
ยทN ๐ท) โ N) โ
โจ(๐ด
ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ โ (N
ร N)) |
4 | 1, 2, 3 | syl2an 289 |
. . 3
โข (((๐ด โ N โง
๐ถ โ N)
โง (๐ต โ
N โง ๐ท
โ N)) โ โจ(๐ด ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ โ (N
ร N)) |
5 | 4 | an4s 588 |
. 2
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ โจ(๐ด ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ โ (N
ร N)) |
6 | | mulclpi 7326 |
. . . 4
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) โ N) |
7 | | mulclpi 7326 |
. . . 4
โข ((๐ โ N โง
โ โ N)
โ (๐
ยทN โ) โ N) |
8 | | opelxpi 4658 |
. . . 4
โข (((๐
ยทN ๐) โ N โง (๐
ยทN โ) โ N) โ โจ(๐
ยทN ๐), (๐ ยทN โ)โฉ โ (N
ร N)) |
9 | 6, 7, 8 | syl2an 289 |
. . 3
โข (((๐ โ N โง
๐ โ N)
โง (๐ โ
N โง โ
โ N)) โ โจ(๐ ยทN ๐), (๐ ยทN โ)โฉ โ (N
ร N)) |
10 | 9 | an4s 588 |
. 2
โข (((๐ โ N โง
๐ โ N)
โง (๐ โ
N โง โ
โ N)) โ โจ(๐ ยทN ๐), (๐ ยทN โ)โฉ โ (N
ร N)) |
11 | | mulclpi 7326 |
. . . 4
โข ((๐ โ N โง
๐ก โ N)
โ (๐
ยทN ๐ก) โ N) |
12 | | mulclpi 7326 |
. . . 4
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐ ) โ N) |
13 | | opelxpi 4658 |
. . . 4
โข (((๐
ยทN ๐ก) โ N โง (๐
ยทN ๐ ) โ N) โ โจ(๐
ยทN ๐ก), (๐ ยทN ๐ )โฉ โ (N
ร N)) |
14 | 11, 12, 13 | syl2an 289 |
. . 3
โข (((๐ โ N โง
๐ก โ N)
โง (๐ โ
N โง ๐
โ N)) โ โจ(๐ ยทN ๐ก), (๐ ยทN ๐ )โฉ โ (N
ร N)) |
15 | 14 | an4s 588 |
. 2
โข (((๐ โ N โง
๐ โ N)
โง (๐ก โ
N โง ๐
โ N)) โ โจ(๐ ยทN ๐ก), (๐ ยทN ๐ )โฉ โ (N
ร N)) |
16 | | enqex 7358 |
. 2
โข
~Q โ V |
17 | | enqer 7356 |
. 2
โข
~Q Er (N ร
N) |
18 | | df-enq 7345 |
. 2
โข
~Q = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ)))} |
19 | | simpll 527 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ ๐ง = ๐) |
20 | | simprr 531 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ ๐ข = ๐) |
21 | 19, 20 | oveq12d 5892 |
. . 3
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ (๐ง ยทN ๐ข) = (๐ ยทN ๐)) |
22 | | simplr 528 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ ๐ค = ๐) |
23 | | simprl 529 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ ๐ฃ = ๐) |
24 | 22, 23 | oveq12d 5892 |
. . 3
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ (๐ค ยทN ๐ฃ) = (๐ ยทN ๐)) |
25 | 21, 24 | eqeq12d 2192 |
. 2
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ ((๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ) โ (๐ ยทN ๐) = (๐ ยทN ๐))) |
26 | | simpll 527 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ ๐ง = ๐) |
27 | | simprr 531 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ ๐ข = ๐ ) |
28 | 26, 27 | oveq12d 5892 |
. . 3
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ (๐ง ยทN ๐ข) = (๐ ยทN ๐ )) |
29 | | simplr 528 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ ๐ค = โ) |
30 | | simprl 529 |
. . . 4
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ ๐ฃ = ๐ก) |
31 | 29, 30 | oveq12d 5892 |
. . 3
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ (๐ค ยทN ๐ฃ) = (โ ยทN ๐ก)) |
32 | 28, 31 | eqeq12d 2192 |
. 2
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ ((๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ) โ (๐ ยทN ๐ ) = (โ ยทN ๐ก))) |
33 | | dfmpq2 7353 |
. 2
โข
ยทpQ = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ))} |
34 | | simpll 527 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ ๐ค = ๐) |
35 | | simprl 529 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ ๐ข = ๐) |
36 | 34, 35 | oveq12d 5892 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ (๐ค ยทN ๐ข) = (๐ ยทN ๐)) |
37 | | simplr 528 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ ๐ฃ = ๐) |
38 | | simprr 531 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ ๐ = โ) |
39 | 37, 38 | oveq12d 5892 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ (๐ฃ ยทN ๐) = (๐ ยทN โ)) |
40 | 36, 39 | opeq12d 3786 |
. 2
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ = โจ(๐
ยทN ๐), (๐ ยทN โ)โฉ) |
41 | | simpll 527 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ ๐ค = ๐) |
42 | | simprl 529 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ ๐ข = ๐ก) |
43 | 41, 42 | oveq12d 5892 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ (๐ค ยทN ๐ข) = (๐ ยทN ๐ก)) |
44 | | simplr 528 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ ๐ฃ = ๐) |
45 | | simprr 531 |
. . . 4
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ ๐ = ๐ ) |
46 | 44, 45 | oveq12d 5892 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ (๐ฃ ยทN ๐) = (๐ ยทN ๐ )) |
47 | 43, 46 | opeq12d 3786 |
. 2
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ = โจ(๐
ยทN ๐ก), (๐ ยทN ๐ )โฉ) |
48 | | simpll 527 |
. . . 4
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ ๐ค = ๐ด) |
49 | | simprl 529 |
. . . 4
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ ๐ข = ๐ถ) |
50 | 48, 49 | oveq12d 5892 |
. . 3
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ (๐ค ยทN ๐ข) = (๐ด ยทN ๐ถ)) |
51 | | simplr 528 |
. . . 4
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ ๐ฃ = ๐ต) |
52 | | simprr 531 |
. . . 4
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ ๐ = ๐ท) |
53 | 51, 52 | oveq12d 5892 |
. . 3
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ (๐ฃ ยทN ๐) = (๐ต ยทN ๐ท)) |
54 | 50, 53 | opeq12d 3786 |
. 2
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ = โจ(๐ด
ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ) |
55 | | df-mqqs 7348 |
. 2
โข
ยทQ = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ Q โง ๐ฆ โ Q) โง
โ๐โ๐โ๐โ๐((๐ฅ = [โจ๐, ๐โฉ] ~Q โง
๐ฆ = [โจ๐, ๐โฉ] ~Q ) โง
๐ง = [(โจ๐, ๐โฉ ยทpQ
โจ๐, ๐โฉ)] ~Q
))} |
56 | | df-nqqs 7346 |
. 2
โข
Q = ((N ร N) /
~Q ) |
57 | | mulcmpblnq 7366 |
. 2
โข ((((๐ โ N โง
๐ โ N)
โง (๐ โ
N โง ๐
โ N)) โง ((๐ โ N โง โ โ N) โง
(๐ก โ N
โง ๐ โ
N))) โ (((๐ ยทN ๐) = (๐ ยทN ๐) โง (๐ ยทN ๐ ) = (โ ยทN ๐ก)) โ โจ(๐
ยทN ๐), (๐ ยทN โ)โฉ
~Q โจ(๐ ยทN ๐ก), (๐ ยทN ๐ )โฉ)) |
58 | 5, 10, 15, 16, 17, 18, 25, 32, 33, 40, 47, 54, 55, 56, 57 | oviec 6640 |
1
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ ([โจ๐ด, ๐ตโฉ] ~Q
ยทQ [โจ๐ถ, ๐ทโฉ] ~Q ) =
[โจ(๐ด
ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ]
~Q ) |