Step | Hyp | Ref
| Expression |
1 | | df-nq0 7437 |
. . 3
โข
Q0 = ((ฯ ร N)
/ ~Q0 ) |
2 | | oveq1 5895 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
(๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
3 | 2 | eleq1d 2256 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) โ
((ฯ ร N) / ~Q0 )
โ (๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) โ
((ฯ ร N) / ~Q0
))) |
4 | | oveq2 5896 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ (๐ด ยทQ0
[โจ๐ง, ๐คโฉ]
~Q0 ) = (๐ด ยทQ0 ๐ต)) |
5 | 4 | eleq1d 2256 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ((๐ด ยทQ0
[โจ๐ง, ๐คโฉ]
~Q0 ) โ ((ฯ ร N)
/ ~Q0 ) โ (๐ด ยทQ0 ๐ต) โ ((ฯ ร
N) / ~Q0 ))) |
6 | | mulnnnq0 7462 |
. . . 4
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
[โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 ) |
7 | | nnmcl 6495 |
. . . . . . 7
โข ((๐ฅ โ ฯ โง ๐ง โ ฯ) โ (๐ฅ ยทo ๐ง) โ
ฯ) |
8 | | mulpiord 7329 |
. . . . . . . 8
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) = (๐ฆ ยทo ๐ค)) |
9 | | mulclpi 7340 |
. . . . . . . 8
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) โ N) |
10 | 8, 9 | eqeltrrd 2265 |
. . . . . . 7
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทo ๐ค)
โ N) |
11 | 7, 10 | anim12i 338 |
. . . . . 6
โข (((๐ฅ โ ฯ โง ๐ง โ ฯ) โง (๐ฆ โ N โง
๐ค โ N))
โ ((๐ฅ
ยทo ๐ง)
โ ฯ โง (๐ฆ
ยทo ๐ค)
โ N)) |
12 | 11 | an4s 588 |
. . . . 5
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ((๐ฅ
ยทo ๐ง)
โ ฯ โง (๐ฆ
ยทo ๐ค)
โ N)) |
13 | | opelxpi 4670 |
. . . . 5
โข (((๐ฅ ยทo ๐ง) โ ฯ โง (๐ฆ ยทo ๐ค) โ N) โ
โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ โ (ฯ
ร N)) |
14 | | enq0ex 7451 |
. . . . . 6
โข
~Q0 โ V |
15 | 14 | ecelqsi 6602 |
. . . . 5
โข
(โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ โ (ฯ
ร N) โ [โจ(๐ฅ ยทo ๐ง), (๐ฆ ยทo ๐ค)โฉ] ~Q0 โ
((ฯ ร N) / ~Q0
)) |
16 | 12, 13, 15 | 3syl 17 |
. . . 4
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ [โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 โ ((ฯ ร N) /
~Q0 )) |
17 | 6, 16 | eqeltrd 2264 |
. . 3
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) โ
((ฯ ร N) / ~Q0
)) |
18 | 1, 3, 5, 17 | 2ecoptocl 6636 |
. 2
โข ((๐ด โ
Q0 โง ๐ต โ Q0) โ
(๐ด
ยทQ0 ๐ต) โ ((ฯ ร N)
/ ~Q0 )) |
19 | 18, 1 | eleqtrrdi 2281 |
1
โข ((๐ด โ
Q0 โง ๐ต โ Q0) โ
(๐ด
ยทQ0 ๐ต) โ
Q0) |