Step | Hyp | Ref
| Expression |
1 | | nqercl 10874 |
. . . 4
โข (๐ด โ (N ร
N) โ ([Q]โ๐ด) โ Q) |
2 | | nqercl 10874 |
. . . 4
โข (๐ต โ (N ร
N) โ ([Q]โ๐ต) โ Q) |
3 | | mulpqnq 10884 |
. . . 4
โข
((([Q]โ๐ด) โ Q โง
([Q]โ๐ต)
โ Q) โ (([Q]โ๐ด) ยทQ
([Q]โ๐ต)) =
([Q]โ(([Q]โ๐ด) ยทpQ
([Q]โ๐ต)))) |
4 | 1, 2, 3 | syl2an 597 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ
(([Q]โ๐ด) ยทQ
([Q]โ๐ต)) =
([Q]โ(([Q]โ๐ด) ยทpQ
([Q]โ๐ต)))) |
5 | | enqer 10864 |
. . . . . 6
โข
~Q Er (N ร
N) |
6 | 5 | a1i 11 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ
~Q Er (N ร
N)) |
7 | | nqerrel 10875 |
. . . . . . 7
โข (๐ด โ (N ร
N) โ ๐ด
~Q ([Q]โ๐ด)) |
8 | 7 | adantr 482 |
. . . . . 6
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ๐ด ~Q
([Q]โ๐ด)) |
9 | | elpqn 10868 |
. . . . . . . . 9
โข
(([Q]โ๐ด) โ Q โ
([Q]โ๐ด)
โ (N ร N)) |
10 | 1, 9 | syl 17 |
. . . . . . . 8
โข (๐ด โ (N ร
N) โ ([Q]โ๐ด) โ (N ร
N)) |
11 | | mulerpqlem 10898 |
. . . . . . . . 9
โข ((๐ด โ (N ร
N) โง ([Q]โ๐ด) โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด ~Q
([Q]โ๐ด)
โ (๐ด
ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ ๐ต))) |
12 | 11 | 3exp 1120 |
. . . . . . . 8
โข (๐ด โ (N ร
N) โ (([Q]โ๐ด) โ (N ร
N) โ (๐ต
โ (N ร N) โ (๐ด ~Q
([Q]โ๐ด)
โ (๐ด
ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ ๐ต))))) |
13 | 10, 12 | mpd 15 |
. . . . . . 7
โข (๐ด โ (N ร
N) โ (๐ต
โ (N ร N) โ (๐ด ~Q
([Q]โ๐ด)
โ (๐ด
ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ ๐ต)))) |
14 | 13 | imp 408 |
. . . . . 6
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด ~Q
([Q]โ๐ด)
โ (๐ด
ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ ๐ต))) |
15 | 8, 14 | mpbid 231 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ ๐ต)) |
16 | | nqerrel 10875 |
. . . . . . . 8
โข (๐ต โ (N ร
N) โ ๐ต
~Q ([Q]โ๐ต)) |
17 | 16 | adantl 483 |
. . . . . . 7
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ๐ต ~Q
([Q]โ๐ต)) |
18 | | elpqn 10868 |
. . . . . . . . . 10
โข
(([Q]โ๐ต) โ Q โ
([Q]โ๐ต)
โ (N ร N)) |
19 | 2, 18 | syl 17 |
. . . . . . . . 9
โข (๐ต โ (N ร
N) โ ([Q]โ๐ต) โ (N ร
N)) |
20 | | mulerpqlem 10898 |
. . . . . . . . . 10
โข ((๐ต โ (N ร
N) โง ([Q]โ๐ต) โ (N ร
N) โง ([Q]โ๐ด) โ (N ร
N)) โ (๐ต
~Q ([Q]โ๐ต) โ (๐ต ยทpQ
([Q]โ๐ด)) ~Q
(([Q]โ๐ต) ยทpQ
([Q]โ๐ด)))) |
21 | 20 | 3exp 1120 |
. . . . . . . . 9
โข (๐ต โ (N ร
N) โ (([Q]โ๐ต) โ (N ร
N) โ (([Q]โ๐ด) โ (N ร
N) โ (๐ต
~Q ([Q]โ๐ต) โ (๐ต ยทpQ
([Q]โ๐ด)) ~Q
(([Q]โ๐ต) ยทpQ
([Q]โ๐ด)))))) |
22 | 19, 21 | mpd 15 |
. . . . . . . 8
โข (๐ต โ (N ร
N) โ (([Q]โ๐ด) โ (N ร
N) โ (๐ต
~Q ([Q]โ๐ต) โ (๐ต ยทpQ
([Q]โ๐ด)) ~Q
(([Q]โ๐ต) ยทpQ
([Q]โ๐ด))))) |
23 | 10, 22 | mpan9 508 |
. . . . . . 7
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ต ~Q
([Q]โ๐ต)
โ (๐ต
ยทpQ ([Q]โ๐ด)) ~Q
(([Q]โ๐ต) ยทpQ
([Q]โ๐ด)))) |
24 | 17, 23 | mpbid 231 |
. . . . . 6
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ต ยทpQ
([Q]โ๐ด)) ~Q
(([Q]โ๐ต) ยทpQ
([Q]โ๐ด))) |
25 | | mulcompq 10895 |
. . . . . 6
โข (๐ต
ยทpQ ([Q]โ๐ด)) = (([Q]โ๐ด)
ยทpQ ๐ต) |
26 | | mulcompq 10895 |
. . . . . 6
โข
(([Q]โ๐ต) ยทpQ
([Q]โ๐ด)) = (([Q]โ๐ด)
ยทpQ ([Q]โ๐ต)) |
27 | 24, 25, 26 | 3brtr3g 5143 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ
(([Q]โ๐ด) ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ
([Q]โ๐ต))) |
28 | 6, 15, 27 | ertrd 8671 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ
([Q]โ๐ต))) |
29 | | mulpqf 10889 |
. . . . . 6
โข
ยทpQ :((N ร N)
ร (N ร N))โถ(N
ร N) |
30 | 29 | fovcl 7489 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด ยทpQ ๐ต) โ (N
ร N)) |
31 | 29 | fovcl 7489 |
. . . . . 6
โข
((([Q]โ๐ด) โ (N ร
N) โง ([Q]โ๐ต) โ (N ร
N)) โ (([Q]โ๐ด) ยทpQ
([Q]โ๐ต)) โ (N ร
N)) |
32 | 10, 19, 31 | syl2an 597 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ
(([Q]โ๐ด) ยทpQ
([Q]โ๐ต)) โ (N ร
N)) |
33 | | nqereq 10878 |
. . . . 5
โข (((๐ด
ยทpQ ๐ต) โ (N ร
N) โง (([Q]โ๐ด) ยทpQ
([Q]โ๐ต)) โ (N ร
N)) โ ((๐ด ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ
([Q]โ๐ต)) โ ([Q]โ(๐ด
ยทpQ ๐ต)) =
([Q]โ(([Q]โ๐ด) ยทpQ
([Q]โ๐ต))))) |
34 | 30, 32, 33 | syl2anc 585 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ((๐ด ยทpQ ๐ต) ~Q
(([Q]โ๐ด) ยทpQ
([Q]โ๐ต)) โ ([Q]โ(๐ด
ยทpQ ๐ต)) =
([Q]โ(([Q]โ๐ด) ยทpQ
([Q]โ๐ต))))) |
35 | 28, 34 | mpbid 231 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ
([Q]โ(๐ด
ยทpQ ๐ต)) =
([Q]โ(([Q]โ๐ด) ยทpQ
([Q]โ๐ต)))) |
36 | 4, 35 | eqtr4d 2780 |
. 2
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ
(([Q]โ๐ด) ยทQ
([Q]โ๐ต)) = ([Q]โ(๐ด
ยทpQ ๐ต))) |
37 | | 0nnq 10867 |
. . . . . . 7
โข ยฌ
โ
โ Q |
38 | | nqerf 10873 |
. . . . . . . . . . 11
โข
[Q]:(N ร
N)โถQ |
39 | 38 | fdmi 6685 |
. . . . . . . . . 10
โข dom
[Q] = (N ร N) |
40 | 39 | eleq2i 2830 |
. . . . . . . . 9
โข (๐ด โ dom [Q]
โ ๐ด โ
(N ร N)) |
41 | | ndmfv 6882 |
. . . . . . . . 9
โข (ยฌ
๐ด โ dom
[Q] โ ([Q]โ๐ด) = โ
) |
42 | 40, 41 | sylnbir 331 |
. . . . . . . 8
โข (ยฌ
๐ด โ (N
ร N) โ ([Q]โ๐ด) = โ
) |
43 | 42 | eleq1d 2823 |
. . . . . . 7
โข (ยฌ
๐ด โ (N
ร N) โ (([Q]โ๐ด) โ Q โ โ
โ Q)) |
44 | 37, 43 | mtbiri 327 |
. . . . . 6
โข (ยฌ
๐ด โ (N
ร N) โ ยฌ ([Q]โ๐ด) โ
Q) |
45 | 44 | con4i 114 |
. . . . 5
โข
(([Q]โ๐ด) โ Q โ ๐ด โ (N ร
N)) |
46 | 39 | eleq2i 2830 |
. . . . . . . . 9
โข (๐ต โ dom [Q]
โ ๐ต โ
(N ร N)) |
47 | | ndmfv 6882 |
. . . . . . . . 9
โข (ยฌ
๐ต โ dom
[Q] โ ([Q]โ๐ต) = โ
) |
48 | 46, 47 | sylnbir 331 |
. . . . . . . 8
โข (ยฌ
๐ต โ (N
ร N) โ ([Q]โ๐ต) = โ
) |
49 | 48 | eleq1d 2823 |
. . . . . . 7
โข (ยฌ
๐ต โ (N
ร N) โ (([Q]โ๐ต) โ Q โ โ
โ Q)) |
50 | 37, 49 | mtbiri 327 |
. . . . . 6
โข (ยฌ
๐ต โ (N
ร N) โ ยฌ ([Q]โ๐ต) โ
Q) |
51 | 50 | con4i 114 |
. . . . 5
โข
(([Q]โ๐ต) โ Q โ ๐ต โ (N ร
N)) |
52 | 45, 51 | anim12i 614 |
. . . 4
โข
((([Q]โ๐ด) โ Q โง
([Q]โ๐ต)
โ Q) โ (๐ด โ (N ร
N) โง ๐ต
โ (N ร N))) |
53 | | mulnqf 10892 |
. . . . . 6
โข
ยทQ :(Q ร
Q)โถQ |
54 | 53 | fdmi 6685 |
. . . . 5
โข dom
ยทQ = (Q ร
Q) |
55 | 54 | ndmov 7543 |
. . . 4
โข (ยฌ
(([Q]โ๐ด) โ Q โง
([Q]โ๐ต)
โ Q) โ (([Q]โ๐ด) ยทQ
([Q]โ๐ต)) = โ
) |
56 | 52, 55 | nsyl5 159 |
. . 3
โข (ยฌ
(๐ด โ (N
ร N) โง ๐ต โ (N ร
N)) โ (([Q]โ๐ด) ยทQ
([Q]โ๐ต)) = โ
) |
57 | | 0nelxp 5672 |
. . . . . 6
โข ยฌ
โ
โ (N ร N) |
58 | 39 | eleq2i 2830 |
. . . . . 6
โข (โ
โ dom [Q] โ โ
โ (N ร
N)) |
59 | 57, 58 | mtbir 323 |
. . . . 5
โข ยฌ
โ
โ dom [Q] |
60 | 29 | fdmi 6685 |
. . . . . . 7
โข dom
ยทpQ = ((N ร
N) ร (N ร
N)) |
61 | 60 | ndmov 7543 |
. . . . . 6
โข (ยฌ
(๐ด โ (N
ร N) โง ๐ต โ (N ร
N)) โ (๐ด
ยทpQ ๐ต) = โ
) |
62 | 61 | eleq1d 2823 |
. . . . 5
โข (ยฌ
(๐ด โ (N
ร N) โง ๐ต โ (N ร
N)) โ ((๐ด ยทpQ ๐ต) โ dom [Q]
โ โ
โ dom [Q])) |
63 | 59, 62 | mtbiri 327 |
. . . 4
โข (ยฌ
(๐ด โ (N
ร N) โง ๐ต โ (N ร
N)) โ ยฌ (๐ด ยทpQ ๐ต) โ dom
[Q]) |
64 | | ndmfv 6882 |
. . . 4
โข (ยฌ
(๐ด
ยทpQ ๐ต) โ dom [Q] โ
([Q]โ(๐ด
ยทpQ ๐ต)) = โ
) |
65 | 63, 64 | syl 17 |
. . 3
โข (ยฌ
(๐ด โ (N
ร N) โง ๐ต โ (N ร
N)) โ ([Q]โ(๐ด ยทpQ ๐ต)) = โ
) |
66 | 56, 65 | eqtr4d 2780 |
. 2
โข (ยฌ
(๐ด โ (N
ร N) โง ๐ต โ (N ร
N)) โ (([Q]โ๐ด) ยทQ
([Q]โ๐ต)) = ([Q]โ(๐ด
ยทpQ ๐ต))) |
67 | 36, 66 | pm2.61i 182 |
1
โข
(([Q]โ๐ด) ยทQ
([Q]โ๐ต)) = ([Q]โ(๐ด
ยทpQ ๐ต)) |