Step | Hyp | Ref
| Expression |
1 | | df-nq0 7424 |
. 2
โข
Q0 = ((ฯ ร N)
/ ~Q0 ) |
2 | | oveq1 5882 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
(๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
3 | | oveq2 5883 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 [โจ๐ฅ, ๐ฆโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 ๐ด)) |
4 | 2, 3 | eqeq12d 2192 |
. 2
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 [โจ๐ฅ, ๐ฆโฉ] ~Q0 ) โ
(๐ด
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 ๐ด))) |
5 | | oveq2 5883 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ (๐ด ยทQ0
[โจ๐ง, ๐คโฉ]
~Q0 ) = (๐ด ยทQ0 ๐ต)) |
6 | | oveq1 5882 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 ๐ด) = (๐ต ยทQ0 ๐ด)) |
7 | 5, 6 | eqeq12d 2192 |
. 2
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ((๐ด ยทQ0
[โจ๐ง, ๐คโฉ]
~Q0 ) = ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 ๐ด) โ (๐ด ยทQ0 ๐ต) = (๐ต ยทQ0 ๐ด))) |
8 | | nnmcom 6490 |
. . . . 5
โข ((๐ฅ โ ฯ โง ๐ง โ ฯ) โ (๐ฅ ยทo ๐ง) = (๐ง ยทo ๐ฅ)) |
9 | 8 | ad2ant2r 509 |
. . . 4
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ (๐ฅ
ยทo ๐ง) =
(๐ง ยทo
๐ฅ)) |
10 | | pinn 7308 |
. . . . . 6
โข (๐ฆ โ N โ
๐ฆ โ
ฯ) |
11 | | pinn 7308 |
. . . . . 6
โข (๐ค โ N โ
๐ค โ
ฯ) |
12 | | nnmcom 6490 |
. . . . . 6
โข ((๐ฆ โ ฯ โง ๐ค โ ฯ) โ (๐ฆ ยทo ๐ค) = (๐ค ยทo ๐ฆ)) |
13 | 10, 11, 12 | syl2an 289 |
. . . . 5
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทo ๐ค) =
(๐ค ยทo
๐ฆ)) |
14 | 13 | ad2ant2l 508 |
. . . 4
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ (๐ฆ
ยทo ๐ค) =
(๐ค ยทo
๐ฆ)) |
15 | | opeq12 3781 |
. . . . 5
โข (((๐ฅ ยทo ๐ง) = (๐ง ยทo ๐ฅ) โง (๐ฆ ยทo ๐ค) = (๐ค ยทo ๐ฆ)) โ โจ(๐ฅ ยทo ๐ง), (๐ฆ ยทo ๐ค)โฉ = โจ(๐ง ยทo ๐ฅ), (๐ค ยทo ๐ฆ)โฉ) |
16 | 15 | eceq1d 6571 |
. . . 4
โข (((๐ฅ ยทo ๐ง) = (๐ง ยทo ๐ฅ) โง (๐ฆ ยทo ๐ค) = (๐ค ยทo ๐ฆ)) โ [โจ(๐ฅ ยทo ๐ง), (๐ฆ ยทo ๐ค)โฉ] ~Q0 =
[โจ(๐ง
ยทo ๐ฅ),
(๐ค ยทo
๐ฆ)โฉ]
~Q0 ) |
17 | 9, 14, 16 | syl2anc 411 |
. . 3
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ [โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 = [โจ(๐ง ยทo ๐ฅ), (๐ค ยทo ๐ฆ)โฉ] ~Q0
) |
18 | | mulnnnq0 7449 |
. . 3
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
[โจ(๐ฅ
ยทo ๐ง),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 ) |
19 | | mulnnnq0 7449 |
. . . 4
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฅ โ ฯ โง
๐ฆ โ N))
โ ([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 [โจ๐ฅ, ๐ฆโฉ] ~Q0 ) =
[โจ(๐ง
ยทo ๐ฅ),
(๐ค ยทo
๐ฆ)โฉ]
~Q0 ) |
20 | 19 | ancoms 268 |
. . 3
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 [โจ๐ฅ, ๐ฆโฉ] ~Q0 ) =
[โจ(๐ง
ยทo ๐ฅ),
(๐ค ยทo
๐ฆ)โฉ]
~Q0 ) |
21 | 17, 18, 20 | 3eqtr4d 2220 |
. 2
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 [โจ๐ฅ, ๐ฆโฉ] ~Q0
)) |
22 | 1, 4, 7, 21 | 2ecoptocl 6623 |
1
โข ((๐ด โ
Q0 โง ๐ต โ Q0) โ
(๐ด
ยทQ0 ๐ต) = (๐ต ยทQ0 ๐ด)) |