Step | Hyp | Ref
| Expression |
1 | | enq0er 7433 |
. . 3
โข
~Q0 Er (ฯ ร
N) |
2 | 1 | a1i 9 |
. 2
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ ~Q0 Er (ฯ ร
N)) |
3 | | pinn 7307 |
. . . . 5
โข (๐ด โ N โ
๐ด โ
ฯ) |
4 | 3 | 3ad2ant1 1018 |
. . . 4
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ ๐ด โ
ฯ) |
5 | | simp2 998 |
. . . 4
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ ๐ต โ
ฯ) |
6 | | pinn 7307 |
. . . . 5
โข (๐ถ โ N โ
๐ถ โ
ฯ) |
7 | 6 | 3ad2ant3 1020 |
. . . 4
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ ๐ถ โ
ฯ) |
8 | | nnmcom 6489 |
. . . . 5
โข ((๐ฅ โ ฯ โง ๐ฆ โ ฯ) โ (๐ฅ ยทo ๐ฆ) = (๐ฆ ยทo ๐ฅ)) |
9 | 8 | adantl 277 |
. . . 4
โข (((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โง (๐ฅ โ ฯ
โง ๐ฆ โ ฯ))
โ (๐ฅ
ยทo ๐ฆ) =
(๐ฆ ยทo
๐ฅ)) |
10 | | nnmass 6487 |
. . . . 5
โข ((๐ฅ โ ฯ โง ๐ฆ โ ฯ โง ๐ง โ ฯ) โ ((๐ฅ ยทo ๐ฆ) ยทo ๐ง) = (๐ฅ ยทo (๐ฆ ยทo ๐ง))) |
11 | 10 | adantl 277 |
. . . 4
โข (((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โง (๐ฅ โ ฯ
โง ๐ฆ โ ฯ
โง ๐ง โ ฯ))
โ ((๐ฅ
ยทo ๐ฆ)
ยทo ๐ง) =
(๐ฅ ยทo
(๐ฆ ยทo
๐ง))) |
12 | 4, 5, 7, 9, 11 | caov32d 6054 |
. . 3
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ ((๐ด
ยทo ๐ต)
ยทo ๐ถ) =
((๐ด ยทo
๐ถ) ยทo
๐ต)) |
13 | | nnmcl 6481 |
. . . . . . . 8
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ด ยทo ๐ต) โ
ฯ) |
14 | 3, 13 | sylan 283 |
. . . . . . 7
โข ((๐ด โ N โง
๐ต โ ฯ) โ
(๐ด ยทo
๐ต) โ
ฯ) |
15 | | mulpiord 7315 |
. . . . . . . 8
โข ((๐ด โ N โง
๐ถ โ N)
โ (๐ด
ยทN ๐ถ) = (๐ด ยทo ๐ถ)) |
16 | | mulclpi 7326 |
. . . . . . . 8
โข ((๐ด โ N โง
๐ถ โ N)
โ (๐ด
ยทN ๐ถ) โ N) |
17 | 15, 16 | eqeltrrd 2255 |
. . . . . . 7
โข ((๐ด โ N โง
๐ถ โ N)
โ (๐ด
ยทo ๐ถ)
โ N) |
18 | 14, 17 | anim12i 338 |
. . . . . 6
โข (((๐ด โ N โง
๐ต โ ฯ) โง
(๐ด โ N
โง ๐ถ โ
N)) โ ((๐ด ยทo ๐ต) โ ฯ โง (๐ด ยทo ๐ถ) โ N)) |
19 | | simpr 110 |
. . . . . . 7
โข (((๐ด โ N โง
๐ด โ N)
โง (๐ต โ ฯ
โง ๐ถ โ
N)) โ (๐ต
โ ฯ โง ๐ถ
โ N)) |
20 | 19 | an4s 588 |
. . . . . 6
โข (((๐ด โ N โง
๐ต โ ฯ) โง
(๐ด โ N
โง ๐ถ โ
N)) โ (๐ต
โ ฯ โง ๐ถ
โ N)) |
21 | 18, 20 | jca 306 |
. . . . 5
โข (((๐ด โ N โง
๐ต โ ฯ) โง
(๐ด โ N
โง ๐ถ โ
N)) โ (((๐ด ยทo ๐ต) โ ฯ โง (๐ด ยทo ๐ถ) โ N) โง (๐ต โ ฯ โง ๐ถ โ
N))) |
22 | 21 | 3impdi 1293 |
. . . 4
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ (((๐ด
ยทo ๐ต)
โ ฯ โง (๐ด
ยทo ๐ถ)
โ N) โง (๐ต โ ฯ โง ๐ถ โ N))) |
23 | | enq0breq 7434 |
. . . 4
โข ((((๐ด ยทo ๐ต) โ ฯ โง (๐ด ยทo ๐ถ) โ N) โง
(๐ต โ ฯ โง
๐ถ โ N))
โ (โจ(๐ด
ยทo ๐ต),
(๐ด ยทo
๐ถ)โฉ
~Q0 โจ๐ต, ๐ถโฉ โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = ((๐ด ยทo ๐ถ) ยทo ๐ต))) |
24 | 22, 23 | syl 14 |
. . 3
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ (โจ(๐ด
ยทo ๐ต),
(๐ด ยทo
๐ถ)โฉ
~Q0 โจ๐ต, ๐ถโฉ โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = ((๐ด ยทo ๐ถ) ยทo ๐ต))) |
25 | 12, 24 | mpbird 167 |
. 2
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ โจ(๐ด
ยทo ๐ต),
(๐ด ยทo
๐ถ)โฉ
~Q0 โจ๐ต, ๐ถโฉ) |
26 | 2, 25 | erthi 6580 |
1
โข ((๐ด โ N โง
๐ต โ ฯ โง
๐ถ โ N)
โ [โจ(๐ด
ยทo ๐ต),
(๐ด ยทo
๐ถ)โฉ]
~Q0 = [โจ๐ต, ๐ถโฉ] ~Q0
) |