Step | Hyp | Ref
| Expression |
1 | | rrxlines.e |
. . . . 5
โข ๐ธ = (โ^โ๐ผ) |
2 | | rrxlines.p |
. . . . 5
โข ๐ = (โ โm
๐ผ) |
3 | | rrxlines.l |
. . . . 5
โข ๐ฟ = (LineMโ๐ธ) |
4 | | rrxlines.m |
. . . . 5
โข ยท = (
ยท๐ โ๐ธ) |
5 | | rrxlines.a |
. . . . 5
โข + =
(+gโ๐ธ) |
6 | 1, 2, 3, 4, 5 | rrxlines 47676 |
. . . 4
โข (๐ผ โ Fin โ ๐ฟ = (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))})) |
7 | 6 | oveqd 7421 |
. . 3
โข (๐ผ โ Fin โ (๐๐ฟ๐) = (๐(๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))})๐)) |
8 | 7 | adantr 480 |
. 2
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ (๐๐ฟ๐) = (๐(๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))})๐)) |
9 | | eqidd 2727 |
. . 3
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))}) = (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))})) |
10 | | simpl 482 |
. . . . . . . . 9
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฅ = ๐) |
11 | 10 | oveq2d 7420 |
. . . . . . . 8
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((1 โ ๐ก) ยท ๐ฅ) = ((1 โ ๐ก) ยท ๐)) |
12 | | simpr 484 |
. . . . . . . . 9
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฆ = ๐) |
13 | 12 | oveq2d 7420 |
. . . . . . . 8
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ก ยท ๐ฆ) = (๐ก ยท ๐)) |
14 | 11, 13 | oveq12d 7422 |
. . . . . . 7
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ)) = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐))) |
15 | 14 | eqeq2d 2737 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ)) โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐)))) |
16 | 15 | rexbidv 3172 |
. . . . 5
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ)) โ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐)))) |
17 | 16 | rabbidv 3434 |
. . . 4
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))} = {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐))}) |
18 | 17 | adantl 481 |
. . 3
โข (((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))} = {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐))}) |
19 | | sneq 4633 |
. . . . 5
โข (๐ฅ = ๐ โ {๐ฅ} = {๐}) |
20 | 19 | difeq2d 4117 |
. . . 4
โข (๐ฅ = ๐ โ (๐ โ {๐ฅ}) = (๐ โ {๐})) |
21 | 20 | adantl 481 |
. . 3
โข (((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โง ๐ฅ = ๐) โ (๐ โ {๐ฅ}) = (๐ โ {๐})) |
22 | | simpr1 1191 |
. . 3
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
23 | | id 22 |
. . . . . . . 8
โข (๐ โ ๐ โ ๐ โ ๐) |
24 | 23 | necomd 2990 |
. . . . . . 7
โข (๐ โ ๐ โ ๐ โ ๐) |
25 | 24 | anim2i 616 |
. . . . . 6
โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐ โง ๐ โ ๐)) |
26 | 25 | 3adant1 1127 |
. . . . 5
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐ โง ๐ โ ๐)) |
27 | | eldifsn 4785 |
. . . . 5
โข (๐ โ (๐ โ {๐}) โ (๐ โ ๐ โง ๐ โ ๐)) |
28 | 26, 27 | sylibr 233 |
. . . 4
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ (๐ โ {๐})) |
29 | 28 | adantl 481 |
. . 3
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ (๐ โ {๐})) |
30 | 2 | ovexi 7438 |
. . . . 5
โข ๐ โ V |
31 | 30 | rabex 5325 |
. . . 4
โข {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐))} โ V |
32 | 31 | a1i 11 |
. . 3
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐))} โ V) |
33 | 9, 18, 21, 22, 29, 32 | ovmpodx 7554 |
. 2
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐ฅ) + (๐ก ยท ๐ฆ))})๐) = {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐))}) |
34 | 8, 33 | eqtrd 2766 |
1
โข ((๐ผ โ Fin โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ โ๐ก โ โ ๐ = (((1 โ ๐ก) ยท ๐) + (๐ก ยท ๐))}) |