Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ต โ (๐ด ยทN ๐) = (๐ด ยทN ๐ต)) |
2 | 1 | opeq1d 4841 |
. . . . . 6
โข (๐ = ๐ต โ โจ(๐ด ยทN ๐), (๐ด ยทN ๐)โฉ = โจ(๐ด
ยทN ๐ต), (๐ด ยทN ๐)โฉ) |
3 | | opeq1 4835 |
. . . . . 6
โข (๐ = ๐ต โ โจ๐, ๐โฉ = โจ๐ต, ๐โฉ) |
4 | 2, 3 | breq12d 5123 |
. . . . 5
โข (๐ = ๐ต โ (โจ(๐ด ยทN ๐), (๐ด ยทN ๐)โฉ
~Q โจ๐, ๐โฉ โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐)โฉ
~Q โจ๐ต, ๐โฉ)) |
5 | 4 | imbi2d 341 |
. . . 4
โข (๐ = ๐ต โ ((๐ด โ N โ โจ(๐ด
ยทN ๐), (๐ด ยทN ๐)โฉ
~Q โจ๐, ๐โฉ) โ (๐ด โ N โ โจ(๐ด
ยทN ๐ต), (๐ด ยทN ๐)โฉ
~Q โจ๐ต, ๐โฉ))) |
6 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ถ โ (๐ด ยทN ๐) = (๐ด ยทN ๐ถ)) |
7 | 6 | opeq2d 4842 |
. . . . . 6
โข (๐ = ๐ถ โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐)โฉ = โจ(๐ด
ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ) |
8 | | opeq2 4836 |
. . . . . 6
โข (๐ = ๐ถ โ โจ๐ต, ๐โฉ = โจ๐ต, ๐ถโฉ) |
9 | 7, 8 | breq12d 5123 |
. . . . 5
โข (๐ = ๐ถ โ (โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐)โฉ
~Q โจ๐ต, ๐โฉ โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ)) |
10 | 9 | imbi2d 341 |
. . . 4
โข (๐ = ๐ถ โ ((๐ด โ N โ โจ(๐ด
ยทN ๐ต), (๐ด ยทN ๐)โฉ
~Q โจ๐ต, ๐โฉ) โ (๐ด โ N โ โจ(๐ด
ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ))) |
11 | | mulcompi 10839 |
. . . . . . . . 9
โข (๐
ยทN ๐) = (๐ ยทN ๐) |
12 | 11 | oveq2i 7373 |
. . . . . . . 8
โข (๐ด
ยทN (๐ ยทN ๐)) = (๐ด ยทN (๐
ยทN ๐)) |
13 | | mulasspi 10840 |
. . . . . . . 8
โข ((๐ด
ยทN ๐) ยทN ๐) = (๐ด ยทN (๐
ยทN ๐)) |
14 | | mulasspi 10840 |
. . . . . . . 8
โข ((๐ด
ยทN ๐) ยทN ๐) = (๐ด ยทN (๐
ยทN ๐)) |
15 | 12, 13, 14 | 3eqtr4i 2775 |
. . . . . . 7
โข ((๐ด
ยทN ๐) ยทN ๐) = ((๐ด ยทN ๐)
ยทN ๐) |
16 | | mulclpi 10836 |
. . . . . . . . 9
โข ((๐ด โ N โง
๐ โ N)
โ (๐ด
ยทN ๐) โ N) |
17 | 16 | 3adant3 1133 |
. . . . . . . 8
โข ((๐ด โ N โง
๐ โ N
โง ๐ โ
N) โ (๐ด
ยทN ๐) โ N) |
18 | | mulclpi 10836 |
. . . . . . . . 9
โข ((๐ด โ N โง
๐ โ N)
โ (๐ด
ยทN ๐) โ N) |
19 | 18 | 3adant2 1132 |
. . . . . . . 8
โข ((๐ด โ N โง
๐ โ N
โง ๐ โ
N) โ (๐ด
ยทN ๐) โ N) |
20 | | 3simpc 1151 |
. . . . . . . 8
โข ((๐ด โ N โง
๐ โ N
โง ๐ โ
N) โ (๐
โ N โง ๐ โ N)) |
21 | | enqbreq 10862 |
. . . . . . . 8
โข ((((๐ด
ยทN ๐) โ N โง (๐ด
ยทN ๐) โ N) โง (๐ โ N โง
๐ โ N))
โ (โจ(๐ด
ยทN ๐), (๐ด ยทN ๐)โฉ
~Q โจ๐, ๐โฉ โ ((๐ด ยทN ๐)
ยทN ๐) = ((๐ด ยทN ๐)
ยทN ๐))) |
22 | 17, 19, 20, 21 | syl21anc 837 |
. . . . . . 7
โข ((๐ด โ N โง
๐ โ N
โง ๐ โ
N) โ (โจ(๐ด ยทN ๐), (๐ด ยทN ๐)โฉ
~Q โจ๐, ๐โฉ โ ((๐ด ยทN ๐)
ยทN ๐) = ((๐ด ยทN ๐)
ยทN ๐))) |
23 | 15, 22 | mpbiri 258 |
. . . . . 6
โข ((๐ด โ N โง
๐ โ N
โง ๐ โ
N) โ โจ(๐ด ยทN ๐), (๐ด ยทN ๐)โฉ
~Q โจ๐, ๐โฉ) |
24 | 23 | 3expb 1121 |
. . . . 5
โข ((๐ด โ N โง
(๐ โ N
โง ๐ โ
N)) โ โจ(๐ด ยทN ๐), (๐ด ยทN ๐)โฉ
~Q โจ๐, ๐โฉ) |
25 | 24 | expcom 415 |
. . . 4
โข ((๐ โ N โง
๐ โ N)
โ (๐ด โ
N โ โจ(๐ด ยทN ๐), (๐ด ยทN ๐)โฉ
~Q โจ๐, ๐โฉ)) |
26 | 5, 10, 25 | vtocl2ga 3538 |
. . 3
โข ((๐ต โ N โง
๐ถ โ N)
โ (๐ด โ
N โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ)) |
27 | 26 | impcom 409 |
. 2
โข ((๐ด โ N โง
(๐ต โ N
โง ๐ถ โ
N)) โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ) |
28 | 27 | 3impb 1116 |
1
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ) |