Step | Hyp | Ref
| Expression |
1 | | rrxlinesc.e |
. . 3
โข ๐ธ = (โ^โ๐ผ) |
2 | | rrxlinesc.p |
. . 3
โข ๐ = (โ โm
๐ผ) |
3 | | rrxlinesc.l |
. . 3
โข ๐ฟ = (LineMโ๐ธ) |
4 | | eqid 2733 |
. . 3
โข (
ยท๐ โ๐ธ) = ( ยท๐
โ๐ธ) |
5 | | eqid 2733 |
. . 3
โข
(+gโ๐ธ) = (+gโ๐ธ) |
6 | 1, 2, 3, 4, 5 | rrxlines 46909 |
. 2
โข (๐ผ โ Fin โ ๐ฟ = (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก)( ยท๐
โ๐ธ)๐ฅ)(+gโ๐ธ)(๐ก( ยท๐
โ๐ธ)๐ฆ))})) |
7 | | eqid 2733 |
. . . . . 6
โข
(Baseโ๐ธ) =
(Baseโ๐ธ) |
8 | | simpll1 1213 |
. . . . . 6
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ ๐ผ โ Fin) |
9 | | 1red 11164 |
. . . . . . 7
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ 1 โ
โ) |
10 | | simpr 486 |
. . . . . . 7
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ ๐ก โ โ) |
11 | 9, 10 | resubcld 11591 |
. . . . . 6
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ (1 โ ๐ก) โ
โ) |
12 | | id 22 |
. . . . . . . . . . . 12
โข (๐ผ โ Fin โ ๐ผ โ Fin) |
13 | 12, 1, 7 | rrxbasefi 24797 |
. . . . . . . . . . 11
โข (๐ผ โ Fin โ
(Baseโ๐ธ) = (โ
โm ๐ผ)) |
14 | 2, 13 | eqtr4id 2792 |
. . . . . . . . . 10
โข (๐ผ โ Fin โ ๐ = (Baseโ๐ธ)) |
15 | 14 | eleq2d 2820 |
. . . . . . . . 9
โข (๐ผ โ Fin โ (๐ฅ โ ๐ โ ๐ฅ โ (Baseโ๐ธ))) |
16 | 15 | biimpa 478 |
. . . . . . . 8
โข ((๐ผ โ Fin โง ๐ฅ โ ๐) โ ๐ฅ โ (Baseโ๐ธ)) |
17 | 16 | 3adant3 1133 |
. . . . . . 7
โข ((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โ ๐ฅ โ (Baseโ๐ธ)) |
18 | 17 | ad2antrr 725 |
. . . . . 6
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ ๐ฅ โ (Baseโ๐ธ)) |
19 | | eldifi 4090 |
. . . . . . . . . 10
โข (๐ฆ โ (๐ โ {๐ฅ}) โ ๐ฆ โ ๐) |
20 | 14 | eleq2d 2820 |
. . . . . . . . . 10
โข (๐ผ โ Fin โ (๐ฆ โ ๐ โ ๐ฆ โ (Baseโ๐ธ))) |
21 | 19, 20 | imbitrid 243 |
. . . . . . . . 9
โข (๐ผ โ Fin โ (๐ฆ โ (๐ โ {๐ฅ}) โ ๐ฆ โ (Baseโ๐ธ))) |
22 | 21 | a1d 25 |
. . . . . . . 8
โข (๐ผ โ Fin โ (๐ฅ โ ๐ โ (๐ฆ โ (๐ โ {๐ฅ}) โ ๐ฆ โ (Baseโ๐ธ)))) |
23 | 22 | 3imp 1112 |
. . . . . . 7
โข ((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โ ๐ฆ โ (Baseโ๐ธ)) |
24 | 23 | ad2antrr 725 |
. . . . . 6
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ ๐ฆ โ (Baseโ๐ธ)) |
25 | 14 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โ ๐ = (Baseโ๐ธ)) |
26 | 25 | eleq2d 2820 |
. . . . . . . 8
โข ((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โ (๐ โ ๐ โ ๐ โ (Baseโ๐ธ))) |
27 | 26 | biimpa 478 |
. . . . . . 7
โข (((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โ ๐ โ (Baseโ๐ธ)) |
28 | 27 | adantr 482 |
. . . . . 6
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ ๐ โ (Baseโ๐ธ)) |
29 | 1, 7, 4, 8, 11, 18, 24, 28, 5, 10 | rrxplusgvscavalb 24782 |
. . . . 5
โข ((((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โง ๐ก โ โ) โ (๐ = (((1 โ ๐ก)( ยท๐
โ๐ธ)๐ฅ)(+gโ๐ธ)(๐ก( ยท๐
โ๐ธ)๐ฆ)) โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐ฅโ๐)) + (๐ก ยท (๐ฆโ๐))))) |
30 | 29 | rexbidva 3170 |
. . . 4
โข (((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โง ๐ โ ๐) โ (โ๐ก โ โ ๐ = (((1 โ ๐ก)( ยท๐
โ๐ธ)๐ฅ)(+gโ๐ธ)(๐ก( ยท๐
โ๐ธ)๐ฆ)) โ โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐ฅโ๐)) + (๐ก ยท (๐ฆโ๐))))) |
31 | 30 | rabbidva 3413 |
. . 3
โข ((๐ผ โ Fin โง ๐ฅ โ ๐ โง ๐ฆ โ (๐ โ {๐ฅ})) โ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก)( ยท๐
โ๐ธ)๐ฅ)(+gโ๐ธ)(๐ก( ยท๐
โ๐ธ)๐ฆ))} = {๐ โ ๐ โฃ โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐ฅโ๐)) + (๐ก ยท (๐ฆโ๐)))}) |
32 | 31 | mpoeq3dva 7438 |
. 2
โข (๐ผ โ Fin โ (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก)( ยท๐
โ๐ธ)๐ฅ)(+gโ๐ธ)(๐ก( ยท๐
โ๐ธ)๐ฆ))}) = (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐ฅโ๐)) + (๐ก ยท (๐ฆโ๐)))})) |
33 | 6, 32 | eqtrd 2773 |
1
โข (๐ผ โ Fin โ ๐ฟ = (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐ก) ยท (๐ฅโ๐)) + (๐ก ยท (๐ฆโ๐)))})) |