Step | Hyp | Ref
| Expression |
1 | | oveq12 5884 |
. 2
โข (((๐ด
ยทN ๐ท) = (๐ต ยทN ๐ถ) โง (๐น ยทN ๐) = (๐บ ยทN ๐
)) โ ((๐ด ยทN ๐ท)
ยทN (๐น ยทN ๐)) = ((๐ต ยทN ๐ถ)
ยทN (๐บ ยทN ๐
))) |
2 | | mulclpi 7327 |
. . . . . . . 8
โข ((๐ด โ N โง
๐น โ N)
โ (๐ด
ยทN ๐น) โ N) |
3 | | mulclpi 7327 |
. . . . . . . 8
โข ((๐ต โ N โง
๐บ โ N)
โ (๐ต
ยทN ๐บ) โ N) |
4 | 2, 3 | anim12i 338 |
. . . . . . 7
โข (((๐ด โ N โง
๐น โ N)
โง (๐ต โ
N โง ๐บ
โ N)) โ ((๐ด ยทN ๐น) โ N โง
(๐ต
ยทN ๐บ) โ N)) |
5 | 4 | an4s 588 |
. . . . . 6
โข (((๐ด โ N โง
๐ต โ N)
โง (๐น โ
N โง ๐บ
โ N)) โ ((๐ด ยทN ๐น) โ N โง
(๐ต
ยทN ๐บ) โ N)) |
6 | | mulclpi 7327 |
. . . . . . . 8
โข ((๐ถ โ N โง
๐
โ N)
โ (๐ถ
ยทN ๐
) โ N) |
7 | | mulclpi 7327 |
. . . . . . . 8
โข ((๐ท โ N โง
๐ โ N)
โ (๐ท
ยทN ๐) โ N) |
8 | 6, 7 | anim12i 338 |
. . . . . . 7
โข (((๐ถ โ N โง
๐
โ N)
โง (๐ท โ
N โง ๐
โ N)) โ ((๐ถ ยทN ๐
) โ N โง
(๐ท
ยทN ๐) โ N)) |
9 | 8 | an4s 588 |
. . . . . 6
โข (((๐ถ โ N โง
๐ท โ N)
โง (๐
โ
N โง ๐
โ N)) โ ((๐ถ ยทN ๐
) โ N โง
(๐ท
ยทN ๐) โ N)) |
10 | 5, 9 | anim12i 338 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐น โ
N โง ๐บ
โ N)) โง ((๐ถ โ N โง ๐ท โ N) โง
(๐
โ N
โง ๐ โ
N))) โ (((๐ด ยทN ๐น) โ N โง
(๐ต
ยทN ๐บ) โ N) โง ((๐ถ
ยทN ๐
) โ N โง (๐ท
ยทN ๐) โ N))) |
11 | 10 | an4s 588 |
. . . 4
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ (((๐ด ยทN ๐น) โ N โง
(๐ต
ยทN ๐บ) โ N) โง ((๐ถ
ยทN ๐
) โ N โง (๐ท
ยทN ๐) โ N))) |
12 | | enqbreq 7355 |
. . . 4
โข ((((๐ด
ยทN ๐น) โ N โง (๐ต
ยทN ๐บ) โ N) โง ((๐ถ
ยทN ๐
) โ N โง (๐ท
ยทN ๐) โ N)) โ
(โจ(๐ด
ยทN ๐น), (๐ต ยทN ๐บ)โฉ
~Q โจ(๐ถ ยทN ๐
), (๐ท ยทN ๐)โฉ โ ((๐ด
ยทN ๐น) ยทN (๐ท
ยทN ๐)) = ((๐ต ยทN ๐บ)
ยทN (๐ถ ยทN ๐
)))) |
13 | 11, 12 | syl 14 |
. . 3
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ (โจ(๐ด ยทN ๐น), (๐ต ยทN ๐บ)โฉ
~Q โจ(๐ถ ยทN ๐
), (๐ท ยทN ๐)โฉ โ ((๐ด
ยทN ๐น) ยทN (๐ท
ยทN ๐)) = ((๐ต ยทN ๐บ)
ยทN (๐ถ ยทN ๐
)))) |
14 | | simplll 533 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐ด
โ N) |
15 | | simprll 537 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐น
โ N) |
16 | | simplrr 536 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐ท
โ N) |
17 | | mulcompig 7330 |
. . . . . 6
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ)) |
18 | 17 | adantl 277 |
. . . . 5
โข
(((((๐ด โ
N โง ๐ต
โ N) โง (๐ถ โ N โง ๐ท โ N)) โง
((๐น โ N
โง ๐บ โ
N) โง (๐
โ N โง ๐ โ N))) โง (๐ฅ โ N โง
๐ฆ โ N))
โ (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ)) |
19 | | mulasspig 7331 |
. . . . . 6
โข ((๐ฅ โ N โง
๐ฆ โ N
โง ๐ง โ
N) โ ((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง))) |
20 | 19 | adantl 277 |
. . . . 5
โข
(((((๐ด โ
N โง ๐ต
โ N) โง (๐ถ โ N โง ๐ท โ N)) โง
((๐น โ N
โง ๐บ โ
N) โง (๐
โ N โง ๐ โ N))) โง (๐ฅ โ N โง
๐ฆ โ N
โง ๐ง โ
N)) โ ((๐ฅ ยทN ๐ฆ)
ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง))) |
21 | | simprrr 540 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐
โ N) |
22 | | mulclpi 7327 |
. . . . . 6
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ (๐ฅ
ยทN ๐ฆ) โ N) |
23 | 22 | adantl 277 |
. . . . 5
โข
(((((๐ด โ
N โง ๐ต
โ N) โง (๐ถ โ N โง ๐ท โ N)) โง
((๐น โ N
โง ๐บ โ
N) โง (๐
โ N โง ๐ โ N))) โง (๐ฅ โ N โง
๐ฆ โ N))
โ (๐ฅ
ยทN ๐ฆ) โ N) |
24 | 14, 15, 16, 18, 20, 21, 23 | caov4d 6059 |
. . . 4
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ((๐ด ยทN ๐น)
ยทN (๐ท ยทN ๐)) = ((๐ด ยทN ๐ท)
ยทN (๐น ยทN ๐))) |
25 | | simpllr 534 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐ต
โ N) |
26 | | simprlr 538 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐บ
โ N) |
27 | | simplrl 535 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐ถ
โ N) |
28 | | simprrl 539 |
. . . . 5
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ๐
โ N) |
29 | 25, 26, 27, 18, 20, 28, 23 | caov4d 6059 |
. . . 4
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ ((๐ต ยทN ๐บ)
ยทN (๐ถ ยทN ๐
)) = ((๐ต ยทN ๐ถ)
ยทN (๐บ ยทN ๐
))) |
30 | 24, 29 | eqeq12d 2192 |
. . 3
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ (((๐ด ยทN ๐น)
ยทN (๐ท ยทN ๐)) = ((๐ต ยทN ๐บ)
ยทN (๐ถ ยทN ๐
)) โ ((๐ด ยทN ๐ท)
ยทN (๐น ยทN ๐)) = ((๐ต ยทN ๐ถ)
ยทN (๐บ ยทN ๐
)))) |
31 | 13, 30 | bitrd 188 |
. 2
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ (โจ(๐ด ยทN ๐น), (๐ต ยทN ๐บ)โฉ
~Q โจ(๐ถ ยทN ๐
), (๐ท ยทN ๐)โฉ โ ((๐ด
ยทN ๐ท) ยทN (๐น
ยทN ๐)) = ((๐ต ยทN ๐ถ)
ยทN (๐บ ยทN ๐
)))) |
32 | 1, 31 | imbitrrid 156 |
1
โข ((((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โง ((๐น โ N โง ๐บ โ N) โง
(๐
โ N
โง ๐ โ
N))) โ (((๐ด ยทN ๐ท) = (๐ต ยทN ๐ถ) โง (๐น ยทN ๐) = (๐บ ยทN ๐
)) โ โจ(๐ด
ยทN ๐น), (๐ต ยทN ๐บ)โฉ
~Q โจ(๐ถ ยทN ๐
), (๐ท ยทN ๐)โฉ)) |