Step | Hyp | Ref
| Expression |
1 | | nq0nn 7440 |
. 2
โข (๐ด โ
Q0 โ โ๐งโ๐ค((๐ง โ ฯ โง ๐ค โ N) โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q0
)) |
2 | | 2onn 6521 |
. . . . . . 7
โข
2o โ ฯ |
3 | | 1pi 7313 |
. . . . . . 7
โข
1o โ N |
4 | | mulnnnq0 7448 |
. . . . . . 7
โข
(((2o โ ฯ โง 1o โ
N) โง (๐ง
โ ฯ โง ๐ค
โ N)) โ ([โจ2o, 1oโฉ]
~Q0 ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
[โจ(2o ยทo ๐ง), (1o ยทo ๐ค)โฉ]
~Q0 ) |
5 | 2, 3, 4 | mpanl12 436 |
. . . . . 6
โข ((๐ง โ ฯ โง ๐ค โ N) โ
([โจ2o, 1oโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
[โจ(2o ยทo ๐ง), (1o ยทo ๐ค)โฉ]
~Q0 ) |
6 | | nn2m 6527 |
. . . . . . . . 9
โข (๐ง โ ฯ โ
(2o ยทo ๐ง) = (๐ง +o ๐ง)) |
7 | 6 | adantr 276 |
. . . . . . . 8
โข ((๐ง โ ฯ โง ๐ค โ N) โ
(2o ยทo ๐ง) = (๐ง +o ๐ง)) |
8 | | pinn 7307 |
. . . . . . . . . 10
โข (๐ค โ N โ
๐ค โ
ฯ) |
9 | | 1onn 6520 |
. . . . . . . . . . . 12
โข
1o โ ฯ |
10 | | nnmcom 6489 |
. . . . . . . . . . . 12
โข
((1o โ ฯ โง ๐ค โ ฯ) โ (1o
ยทo ๐ค) =
(๐ค ยทo
1o)) |
11 | 9, 10 | mpan 424 |
. . . . . . . . . . 11
โข (๐ค โ ฯ โ
(1o ยทo ๐ค) = (๐ค ยทo
1o)) |
12 | | nnm1 6525 |
. . . . . . . . . . 11
โข (๐ค โ ฯ โ (๐ค ยทo
1o) = ๐ค) |
13 | 11, 12 | eqtrd 2210 |
. . . . . . . . . 10
โข (๐ค โ ฯ โ
(1o ยทo ๐ค) = ๐ค) |
14 | 8, 13 | syl 14 |
. . . . . . . . 9
โข (๐ค โ N โ
(1o ยทo ๐ค) = ๐ค) |
15 | 14 | adantl 277 |
. . . . . . . 8
โข ((๐ง โ ฯ โง ๐ค โ N) โ
(1o ยทo ๐ค) = ๐ค) |
16 | 7, 15 | opeq12d 3786 |
. . . . . . 7
โข ((๐ง โ ฯ โง ๐ค โ N) โ
โจ(2o ยทo ๐ง), (1o ยทo ๐ค)โฉ = โจ(๐ง +o ๐ง), ๐คโฉ) |
17 | 16 | eceq1d 6570 |
. . . . . 6
โข ((๐ง โ ฯ โง ๐ค โ N) โ
[โจ(2o ยทo ๐ง), (1o ยทo ๐ค)โฉ]
~Q0 = [โจ(๐ง +o ๐ง), ๐คโฉ] ~Q0
) |
18 | | nnanq0 7456 |
. . . . . . 7
โข ((๐ง โ ฯ โง ๐ง โ ฯ โง ๐ค โ N) โ
[โจ(๐ง +o
๐ง), ๐คโฉ] ~Q0 =
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
19 | 18 | 3anidm12 1295 |
. . . . . 6
โข ((๐ง โ ฯ โง ๐ค โ N) โ
[โจ(๐ง +o
๐ง), ๐คโฉ] ~Q0 =
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
20 | 5, 17, 19 | 3eqtrd 2214 |
. . . . 5
โข ((๐ง โ ฯ โง ๐ค โ N) โ
([โจ2o, 1oโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
21 | 20 | adantr 276 |
. . . 4
โข (((๐ง โ ฯ โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q0 ) โ
([โจ2o, 1oโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
22 | | oveq2 5882 |
. . . . . 6
โข (๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โ
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐ด) = ([โจ2o,
1oโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
23 | | id 19 |
. . . . . . 7
โข (๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โ
๐ด = [โจ๐ง, ๐คโฉ] ~Q0
) |
24 | 23, 23 | oveq12d 5892 |
. . . . . 6
โข (๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โ
(๐ด
+Q0 ๐ด) = ([โจ๐ง, ๐คโฉ] ~Q0
+Q0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
25 | 22, 24 | eqeq12d 2192 |
. . . . 5
โข (๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โ
(([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐ด) = (๐ด +Q0 ๐ด) โ ([โจ2o,
1oโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0
))) |
26 | 25 | adantl 277 |
. . . 4
โข (((๐ง โ ฯ โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q0 ) โ
(([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐ด) = (๐ด +Q0 ๐ด) โ ([โจ2o,
1oโฉ] ~Q0
ยทQ0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
([โจ๐ง, ๐คโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0
))) |
27 | 21, 26 | mpbird 167 |
. . 3
โข (((๐ง โ ฯ โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q0 ) โ
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐ด) = (๐ด +Q0 ๐ด)) |
28 | 27 | exlimivv 1896 |
. 2
โข
(โ๐งโ๐ค((๐ง โ ฯ โง ๐ค โ N) โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q0 ) โ
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐ด) = (๐ด +Q0 ๐ด)) |
29 | 1, 28 | syl 14 |
1
โข (๐ด โ
Q0 โ ([โจ2o, 1oโฉ]
~Q0 ยทQ0 ๐ด) = (๐ด +Q0 ๐ด)) |