Step | Hyp | Ref
| Expression |
1 | | rrx2line.i |
. . . 4
โข ๐ผ = {1, 2} |
2 | | prfi 9272 |
. . . 4
โข {1, 2}
โ Fin |
3 | 1, 2 | eqeltri 2830 |
. . 3
โข ๐ผ โ Fin |
4 | | rrx2line.e |
. . . 4
โข ๐ธ = (โ^โ๐ผ) |
5 | | rrx2line.b |
. . . 4
โข ๐ = (โ โm
๐ผ) |
6 | | rrx2line.l |
. . . 4
โข ๐ฟ = (LineMโ๐ธ) |
7 | 4, 5, 6 | rrxlinec 46912 |
. . 3
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))}) |
8 | 3, 7 | mpan 689 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))}) |
9 | 1 | a1i 11 |
. . . . . 6
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ก โ โ) โ ๐ผ = {1, 2}) |
10 | 9 | raleqdv 3312 |
. . . . 5
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ก โ โ) โ (โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ โ {1, 2} (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) |
11 | | 1ex 11159 |
. . . . . 6
โข 1 โ
V |
12 | | 2ex 12238 |
. . . . . 6
โข 2 โ
V |
13 | | fveq2 6846 |
. . . . . . 7
โข (๐ = 1 โ (๐โ๐) = (๐โ1)) |
14 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = 1 โ (๐โ๐) = (๐โ1)) |
15 | 14 | oveq2d 7377 |
. . . . . . . 8
โข (๐ = 1 โ ((1 โ ๐ก) ยท (๐โ๐)) = ((1 โ ๐ก) ยท (๐โ1))) |
16 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = 1 โ (๐โ๐) = (๐โ1)) |
17 | 16 | oveq2d 7377 |
. . . . . . . 8
โข (๐ = 1 โ (๐ก ยท (๐โ๐)) = (๐ก ยท (๐โ1))) |
18 | 15, 17 | oveq12d 7379 |
. . . . . . 7
โข (๐ = 1 โ (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1)))) |
19 | 13, 18 | eqeq12d 2749 |
. . . . . 6
โข (๐ = 1 โ ((๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))))) |
20 | | fveq2 6846 |
. . . . . . 7
โข (๐ = 2 โ (๐โ๐) = (๐โ2)) |
21 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = 2 โ (๐โ๐) = (๐โ2)) |
22 | 21 | oveq2d 7377 |
. . . . . . . 8
โข (๐ = 2 โ ((1 โ ๐ก) ยท (๐โ๐)) = ((1 โ ๐ก) ยท (๐โ2))) |
23 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = 2 โ (๐โ๐) = (๐โ2)) |
24 | 23 | oveq2d 7377 |
. . . . . . . 8
โข (๐ = 2 โ (๐ก ยท (๐โ๐)) = (๐ก ยท (๐โ2))) |
25 | 22, 24 | oveq12d 7379 |
. . . . . . 7
โข (๐ = 2 โ (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) |
26 | 20, 25 | eqeq12d 2749 |
. . . . . 6
โข (๐ = 2 โ ((๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))) |
27 | 11, 12, 19, 26 | ralpr 4665 |
. . . . 5
โข
(โ๐ โ
{1, 2} (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))) |
28 | 10, 27 | bitrdi 287 |
. . . 4
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ก โ โ) โ (โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))))) |
29 | 28 | rexbidva 3170 |
. . 3
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))))) |
30 | 29 | rabbidva 3413 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ {๐ โ ๐ โฃ โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))} = {๐ โ ๐ โฃ โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))}) |
31 | 8, 30 | eqtrd 2773 |
1
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))}) |