Step | Hyp | Ref
| Expression |
1 | | eengbas 28236 |
. . . . 5
β’ (π β β β
(πΌβπ) =
(Baseβ(EEGβπ))) |
2 | 1 | eqcomd 2738 |
. . . 4
β’ (π β β β
(Baseβ(EEGβπ))
= (πΌβπ)) |
3 | | oveq2 7416 |
. . . . . 6
β’ (π = π β (1...π) = (1...π)) |
4 | 3 | oveq2d 7424 |
. . . . 5
β’ (π = π β (β βm
(1...π)) = (β
βm (1...π))) |
5 | | df-ee 28146 |
. . . . 5
β’ πΌ
= (π β β β¦
(β βm (1...π))) |
6 | | ovex 7441 |
. . . . 5
β’ (β
βm (1...π))
β V |
7 | 4, 5, 6 | fvmpt 6998 |
. . . 4
β’ (π β β β
(πΌβπ) =
(β βm (1...π))) |
8 | 2, 7 | eqtrd 2772 |
. . 3
β’ (π β β β
(Baseβ(EEGβπ))
= (β βm (1...π))) |
9 | 2 | ancli 549 |
. . . . 5
β’ (π β β β (π β β β§
(Baseβ(EEGβπ))
= (πΌβπ))) |
10 | 9, 8 | jca 512 |
. . . 4
β’ (π β β β ((π β β β§
(Baseβ(EEGβπ))
= (πΌβπ)) β§
(Baseβ(EEGβπ))
= (β βm (1...π)))) |
11 | | difeq1 4115 |
. . . . 5
β’
((Baseβ(EEGβπ)) = (β βm (1...π)) β
((Baseβ(EEGβπ))
β {π₯}) = ((β
βm (1...π))
β {π₯})) |
12 | 11 | ad2antlr 725 |
. . . 4
β’ ((((π β β β§
(Baseβ(EEGβπ))
= (πΌβπ)) β§
(Baseβ(EEGβπ))
= (β βm (1...π))) β§ π₯ β (Baseβ(EEGβπ))) β
((Baseβ(EEGβπ))
β {π₯}) = ((β
βm (1...π))
β {π₯})) |
13 | 10, 12 | sylan 580 |
. . 3
β’ ((π β β β§ π₯ β
(Baseβ(EEGβπ)))
β ((Baseβ(EEGβπ)) β {π₯}) = ((β βm (1...π)) β {π₯})) |
14 | 8 | adantr 481 |
. . . 4
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β
(Baseβ(EEGβπ))
= (β βm (1...π))) |
15 | | simpll 765 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π β
β) |
16 | 8 | eleq2d 2819 |
. . . . . . . . 9
β’ (π β β β (π₯ β
(Baseβ(EEGβπ))
β π₯ β (β
βm (1...π)))) |
17 | 16 | biimpcd 248 |
. . . . . . . 8
β’ (π₯ β
(Baseβ(EEGβπ))
β (π β β
β π₯ β (β
βm (1...π)))) |
18 | 17 | adantr 481 |
. . . . . . 7
β’ ((π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯})) β (π β β β π₯ β (β
βm (1...π)))) |
19 | 18 | impcom 408 |
. . . . . 6
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β π₯ β (β
βm (1...π))) |
20 | 19 | adantr 481 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π₯ β (β
βm (1...π))) |
21 | 8 | difeq1d 4121 |
. . . . . . . . . 10
β’ (π β β β
((Baseβ(EEGβπ))
β {π₯}) = ((β
βm (1...π))
β {π₯})) |
22 | 21 | eleq2d 2819 |
. . . . . . . . 9
β’ (π β β β (π¦ β
((Baseβ(EEGβπ))
β {π₯}) β π¦ β ((β
βm (1...π))
β {π₯}))) |
23 | 22 | biimpd 228 |
. . . . . . . 8
β’ (π β β β (π¦ β
((Baseβ(EEGβπ))
β {π₯}) β π¦ β ((β
βm (1...π))
β {π₯}))) |
24 | 23 | adantld 491 |
. . . . . . 7
β’ (π β β β ((π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯})) β π¦ β ((β
βm (1...π))
β {π₯}))) |
25 | 24 | imp 407 |
. . . . . 6
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β π¦ β ((β
βm (1...π))
β {π₯})) |
26 | 25 | adantr 481 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π¦ β ((β
βm (1...π))
β {π₯})) |
27 | 14 | eleq2d 2819 |
. . . . . 6
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β
(π β
(Baseβ(EEGβπ))
β π β (β
βm (1...π)))) |
28 | 27 | biimpa 477 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π β (β
βm (1...π))) |
29 | | eenglngeehlnmlem1 47413 |
. . . . . 6
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β ((βπ§ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ)))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
30 | | eenglngeehlnmlem2 47414 |
. . . . . 6
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β (βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β (βπ§ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ)))))) |
31 | 29, 30 | impbid 211 |
. . . . 5
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β ((βπ§ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ)))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
32 | 15, 20, 26, 28, 31 | syl31anc 1373 |
. . . 4
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β ((βπ§ β
(0[,]1)βπ β
(1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ)))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
33 | 14, 32 | rabeqbidva 3448 |
. . 3
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β
{π β
(Baseβ(EEGβπ))
β£ (βπ§ β
(0[,]1)βπ β
(1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ))))} = {π β (β βm
(1...π)) β£
βπ‘ β β
βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))}) |
34 | 8, 13, 33 | mpoeq123dva 7482 |
. 2
β’ (π β β β (π₯ β
(Baseβ(EEGβπ)),
π¦ β
((Baseβ(EEGβπ))
β {π₯}) β¦ {π β
(Baseβ(EEGβπ))
β£ (βπ§ β
(0[,]1)βπ β
(1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ))))}) = (π₯ β (β βm
(1...π)), π¦ β ((β
βm (1...π))
β {π₯}) β¦ {π β (β
βm (1...π))
β£ βπ‘ β
β βπ β
(1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))})) |
35 | | eqid 2732 |
. . 3
β’
(Baseβ(EEGβπ)) = (Baseβ(EEGβπ)) |
36 | | eqid 2732 |
. . 3
β’
(1...π) = (1...π) |
37 | 35, 36 | elntg2 28240 |
. 2
β’ (π β β β
(LineGβ(EEGβπ))
= (π₯ β
(Baseβ(EEGβπ)),
π¦ β
((Baseβ(EEGβπ))
β {π₯}) β¦ {π β
(Baseβ(EEGβπ))
β£ (βπ§ β
(0[,]1)βπ β
(1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ))))})) |
38 | | nnnn0 12478 |
. . . . 5
β’ (π β β β π β
β0) |
39 | | eqid 2732 |
. . . . . 6
β’
(πΌhilβπ) = (πΌhilβπ) |
40 | 39 | ehlval 24930 |
. . . . 5
β’ (π β β0
β (πΌhilβπ) = (β^β(1...π))) |
41 | 38, 40 | syl 17 |
. . . 4
β’ (π β β β
(πΌhilβπ) = (β^β(1...π))) |
42 | 41 | fveq2d 6895 |
. . 3
β’ (π β β β
(LineMβ(πΌhilβπ)) =
(LineMβ(β^β(1...π)))) |
43 | | fzfid 13937 |
. . . 4
β’ (π β β β
(1...π) β
Fin) |
44 | | eqid 2732 |
. . . . 5
β’
(β^β(1...π)) = (β^β(1...π)) |
45 | | eqid 2732 |
. . . . 5
β’ (β
βm (1...π))
= (β βm (1...π)) |
46 | | eqid 2732 |
. . . . 5
β’
(LineMβ(β^β(1...π))) =
(LineMβ(β^β(1...π))) |
47 | 44, 45, 46 | rrxlinesc 47411 |
. . . 4
β’
((1...π) β Fin
β (LineMβ(β^β(1...π))) = (π₯ β (β βm
(1...π)), π¦ β ((β
βm (1...π))
β {π₯}) β¦ {π β (β
βm (1...π))
β£ βπ‘ β
β βπ β
(1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))})) |
48 | 43, 47 | syl 17 |
. . 3
β’ (π β β β
(LineMβ(β^β(1...π))) = (π₯ β (β βm
(1...π)), π¦ β ((β
βm (1...π))
β {π₯}) β¦ {π β (β
βm (1...π))
β£ βπ‘ β
β βπ β
(1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))})) |
49 | 42, 48 | eqtrd 2772 |
. 2
β’ (π β β β
(LineMβ(πΌhilβπ)) = (π₯ β (β βm
(1...π)), π¦ β ((β
βm (1...π))
β {π₯}) β¦ {π β (β
βm (1...π))
β£ βπ‘ β
β βπ β
(1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))})) |
50 | 34, 37, 49 | 3eqtr4d 2782 |
1
β’ (π β β β
(LineGβ(EEGβπ))
= (LineMβ(πΌhilβπ))) |