Step | Hyp | Ref
| Expression |
1 | | eengbas 27979 |
. . . . 5
β’ (π β β β
(πΌβπ) =
(Baseβ(EEGβπ))) |
2 | 1 | eqcomd 2739 |
. . . 4
β’ (π β β β
(Baseβ(EEGβπ))
= (πΌβπ)) |
3 | | oveq2 7369 |
. . . . . 6
β’ (π = π β (1...π) = (1...π)) |
4 | 3 | oveq2d 7377 |
. . . . 5
β’ (π = π β (β βm
(1...π)) = (β
βm (1...π))) |
5 | | df-ee 27889 |
. . . . 5
β’ πΌ
= (π β β β¦
(β βm (1...π))) |
6 | | ovex 7394 |
. . . . 5
β’ (β
βm (1...π))
β V |
7 | 4, 5, 6 | fvmpt 6952 |
. . . 4
β’ (π β β β
(πΌβπ) =
(β βm (1...π))) |
8 | 2, 7 | eqtrd 2773 |
. . 3
β’ (π β β β
(Baseβ(EEGβπ))
= (β βm (1...π))) |
9 | 2 | ancli 550 |
. . . . 5
β’ (π β β β (π β β β§
(Baseβ(EEGβπ))
= (πΌβπ))) |
10 | 9, 8 | jca 513 |
. . . 4
β’ (π β β β ((π β β β§
(Baseβ(EEGβπ))
= (πΌβπ)) β§
(Baseβ(EEGβπ))
= (β βm (1...π)))) |
11 | | difeq1 4079 |
. . . . 5
β’
((Baseβ(EEGβπ)) = (β βm (1...π)) β
((Baseβ(EEGβπ))
β {π₯}) = ((β
βm (1...π))
β {π₯})) |
12 | 11 | ad2antlr 726 |
. . . 4
β’ ((((π β β β§
(Baseβ(EEGβπ))
= (πΌβπ)) β§
(Baseβ(EEGβπ))
= (β βm (1...π))) β§ π₯ β (Baseβ(EEGβπ))) β
((Baseβ(EEGβπ))
β {π₯}) = ((β
βm (1...π))
β {π₯})) |
13 | 10, 12 | sylan 581 |
. . 3
β’ ((π β β β§ π₯ β
(Baseβ(EEGβπ)))
β ((Baseβ(EEGβπ)) β {π₯}) = ((β βm (1...π)) β {π₯})) |
14 | 8 | adantr 482 |
. . . 4
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β
(Baseβ(EEGβπ))
= (β βm (1...π))) |
15 | | simpll 766 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π β
β) |
16 | 8 | eleq2d 2820 |
. . . . . . . . 9
β’ (π β β β (π₯ β
(Baseβ(EEGβπ))
β π₯ β (β
βm (1...π)))) |
17 | 16 | biimpcd 249 |
. . . . . . . 8
β’ (π₯ β
(Baseβ(EEGβπ))
β (π β β
β π₯ β (β
βm (1...π)))) |
18 | 17 | adantr 482 |
. . . . . . 7
β’ ((π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯})) β (π β β β π₯ β (β
βm (1...π)))) |
19 | 18 | impcom 409 |
. . . . . 6
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β π₯ β (β
βm (1...π))) |
20 | 19 | adantr 482 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π₯ β (β
βm (1...π))) |
21 | 8 | difeq1d 4085 |
. . . . . . . . . 10
β’ (π β β β
((Baseβ(EEGβπ))
β {π₯}) = ((β
βm (1...π))
β {π₯})) |
22 | 21 | eleq2d 2820 |
. . . . . . . . 9
β’ (π β β β (π¦ β
((Baseβ(EEGβπ))
β {π₯}) β π¦ β ((β
βm (1...π))
β {π₯}))) |
23 | 22 | biimpd 228 |
. . . . . . . 8
β’ (π β β β (π¦ β
((Baseβ(EEGβπ))
β {π₯}) β π¦ β ((β
βm (1...π))
β {π₯}))) |
24 | 23 | adantld 492 |
. . . . . . 7
β’ (π β β β ((π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯})) β π¦ β ((β
βm (1...π))
β {π₯}))) |
25 | 24 | imp 408 |
. . . . . 6
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β π¦ β ((β
βm (1...π))
β {π₯})) |
26 | 25 | adantr 482 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π¦ β ((β
βm (1...π))
β {π₯})) |
27 | 14 | eleq2d 2820 |
. . . . . 6
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β
(π β
(Baseβ(EEGβπ))
β π β (β
βm (1...π)))) |
28 | 27 | biimpa 478 |
. . . . 5
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
((Baseβ(EEGβπ))
β {π₯}))) β§ π β
(Baseβ(EEGβπ)))
β π β (β
βm (1...π))) |
29 | | eenglngeehlnmlem1 46913 |
. . . . . 6
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β ((βπ§ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ)))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
30 | | eenglngeehlnmlem2 46914 |
. . . . . 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 1374 |
. . . 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 3422 |
. . 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 7435 |
. 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 2733 |
. . 3
β’
(Baseβ(EEGβπ)) = (Baseβ(EEGβπ)) |
36 | | eqid 2733 |
. . 3
β’
(1...π) = (1...π) |
37 | 35, 36 | elntg2 27983 |
. 2
β’ (π β β β
(LineGβ(EEGβπ))
= (π₯ β
(Baseβ(EEGβπ)),
π¦ β
((Baseβ(EEGβπ))
β {π₯}) β¦ {π β
(Baseβ(EEGβπ))
β£ (βπ§ β
(0[,]1)βπ β
(1...π)(πβπ) = (((1 β π§) Β· (π₯βπ)) + (π§ Β· (π¦βπ))) β¨ βπ£ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π£) Β· (πβπ)) + (π£ Β· (π¦βπ))) β¨ βπ€ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π€) Β· (π₯βπ)) + (π€ Β· (πβπ))))})) |
38 | | nnnn0 12428 |
. . . . 5
β’ (π β β β π β
β0) |
39 | | eqid 2733 |
. . . . . 6
β’
(πΌhilβπ) = (πΌhilβπ) |
40 | 39 | ehlval 24801 |
. . . . 5
β’ (π β β0
β (πΌhilβπ) = (β^β(1...π))) |
41 | 38, 40 | syl 17 |
. . . 4
β’ (π β β β
(πΌhilβπ) = (β^β(1...π))) |
42 | 41 | fveq2d 6850 |
. . 3
β’ (π β β β
(LineMβ(πΌhilβπ)) =
(LineMβ(β^β(1...π)))) |
43 | | fzfid 13887 |
. . . 4
β’ (π β β β
(1...π) β
Fin) |
44 | | eqid 2733 |
. . . . 5
β’
(β^β(1...π)) = (β^β(1...π)) |
45 | | eqid 2733 |
. . . . 5
β’ (β
βm (1...π))
= (β βm (1...π)) |
46 | | eqid 2733 |
. . . . 5
β’
(LineMβ(β^β(1...π))) =
(LineMβ(β^β(1...π))) |
47 | 44, 45, 46 | rrxlinesc 46911 |
. . . 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 2773 |
. 2
β’ (π β β β
(LineMβ(πΌhilβπ)) = (π₯ β (β βm
(1...π)), π¦ β ((β
βm (1...π))
β {π₯}) β¦ {π β (β
βm (1...π))
β£ βπ‘ β
β βπ β
(1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))})) |
50 | 34, 37, 49 | 3eqtr4d 2783 |
1
β’ (π β β β
(LineGβ(EEGβπ))
= (LineMβ(πΌhilβπ))) |