Step | Hyp | Ref
| Expression |
1 | | lnoval.7 |
. 2
β’ πΏ = (π LnOp π) |
2 | | fveq2 6843 |
. . . . . 6
β’ (π’ = π β (BaseSetβπ’) = (BaseSetβπ)) |
3 | | lnoval.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π’ = π β (BaseSetβπ’) = π) |
5 | 4 | oveq2d 7374 |
. . . 4
β’ (π’ = π β ((BaseSetβπ€) βm (BaseSetβπ’)) = ((BaseSetβπ€) βm π)) |
6 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π’ = π β ( +π£ βπ’) = ( +π£
βπ)) |
7 | | lnoval.3 |
. . . . . . . . . 10
β’ πΊ = ( +π£
βπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π’ = π β ( +π£ βπ’) = πΊ) |
9 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π’ = π β (
Β·π OLD βπ’) = ( Β·π OLD
βπ)) |
10 | | lnoval.5 |
. . . . . . . . . . 11
β’ π
= (
Β·π OLD βπ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π’ = π β (
Β·π OLD βπ’) = π
) |
12 | 11 | oveqd 7375 |
. . . . . . . . 9
β’ (π’ = π β (π₯( Β·π OLD
βπ’)π¦) = (π₯π
π¦)) |
13 | | eqidd 2734 |
. . . . . . . . 9
β’ (π’ = π β π§ = π§) |
14 | 8, 12, 13 | oveq123d 7379 |
. . . . . . . 8
β’ (π’ = π β ((π₯( Β·π OLD
βπ’)π¦)( +π£ βπ’)π§) = ((π₯π
π¦)πΊπ§)) |
15 | 14 | fveqeq2d 6851 |
. . . . . . 7
β’ (π’ = π β ((π‘β((π₯( Β·π OLD
βπ’)π¦)( +π£ βπ’)π§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) β (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)))) |
16 | 4, 15 | raleqbidv 3318 |
. . . . . 6
β’ (π’ = π β (βπ§ β (BaseSetβπ’)(π‘β((π₯( Β·π OLD
βπ’)π¦)( +π£ βπ’)π§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) β βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)))) |
17 | 4, 16 | raleqbidv 3318 |
. . . . 5
β’ (π’ = π β (βπ¦ β (BaseSetβπ’)βπ§ β (BaseSetβπ’)(π‘β((π₯( Β·π OLD
βπ’)π¦)( +π£ βπ’)π§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)))) |
18 | 17 | ralbidv 3171 |
. . . 4
β’ (π’ = π β (βπ₯ β β βπ¦ β (BaseSetβπ’)βπ§ β (BaseSetβπ’)(π‘β((π₯( Β·π OLD
βπ’)π¦)( +π£ βπ’)π§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) β βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)))) |
19 | 5, 18 | rabeqbidv 3423 |
. . 3
β’ (π’ = π β {π‘ β ((BaseSetβπ€) βm (BaseSetβπ’)) β£ βπ₯ β β βπ¦ β (BaseSetβπ’)βπ§ β (BaseSetβπ’)(π‘β((π₯( Β·π OLD
βπ’)π¦)( +π£ βπ’)π§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§))} = {π‘ β ((BaseSetβπ€) βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§))}) |
20 | | fveq2 6843 |
. . . . . 6
β’ (π€ = π β (BaseSetβπ€) = (BaseSetβπ)) |
21 | | lnoval.2 |
. . . . . 6
β’ π = (BaseSetβπ) |
22 | 20, 21 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β (BaseSetβπ€) = π) |
23 | 22 | oveq1d 7373 |
. . . 4
β’ (π€ = π β ((BaseSetβπ€) βm π) = (π βm π)) |
24 | | fveq2 6843 |
. . . . . . . . 9
β’ (π€ = π β ( +π£ βπ€) = ( +π£
βπ)) |
25 | | lnoval.4 |
. . . . . . . . 9
β’ π» = ( +π£
βπ) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . . 8
β’ (π€ = π β ( +π£ βπ€) = π») |
27 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π€ = π β (
Β·π OLD βπ€) = ( Β·π OLD
βπ)) |
28 | | lnoval.6 |
. . . . . . . . . 10
β’ π = (
Β·π OLD βπ) |
29 | 27, 28 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π€ = π β (
Β·π OLD βπ€) = π) |
30 | 29 | oveqd 7375 |
. . . . . . . 8
β’ (π€ = π β (π₯( Β·π OLD
βπ€)(π‘βπ¦)) = (π₯π(π‘βπ¦))) |
31 | | eqidd 2734 |
. . . . . . . 8
β’ (π€ = π β (π‘βπ§) = (π‘βπ§)) |
32 | 26, 30, 31 | oveq123d 7379 |
. . . . . . 7
β’ (π€ = π β ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§))) |
33 | 32 | eqeq2d 2744 |
. . . . . 6
β’ (π€ = π β ((π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) β (π‘β((π₯π
π¦)πΊπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§)))) |
34 | 33 | 2ralbidv 3209 |
. . . . 5
β’ (π€ = π β (βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§)))) |
35 | 34 | ralbidv 3171 |
. . . 4
β’ (π€ = π β (βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§)) β βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§)))) |
36 | 23, 35 | rabeqbidv 3423 |
. . 3
β’ (π€ = π β {π‘ β ((BaseSetβπ€) βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§))} = {π‘ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§))}) |
37 | | df-lno 29728 |
. . 3
β’ LnOp =
(π’ β NrmCVec, π€ β NrmCVec β¦ {π‘ β ((BaseSetβπ€) βm
(BaseSetβπ’)) β£
βπ₯ β β
βπ¦ β
(BaseSetβπ’)βπ§ β (BaseSetβπ’)(π‘β((π₯( Β·π OLD
βπ’)π¦)( +π£ βπ’)π§)) = ((π₯( Β·π OLD
βπ€)(π‘βπ¦))( +π£ βπ€)(π‘βπ§))}) |
38 | | ovex 7391 |
. . . 4
β’ (π βm π) β V |
39 | 38 | rabex 5290 |
. . 3
β’ {π‘ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§))} β V |
40 | 19, 36, 37, 39 | ovmpo 7516 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec) β (π LnOp π) = {π‘ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§))}) |
41 | 1, 40 | eqtrid 2785 |
1
β’ ((π β NrmCVec β§ π β NrmCVec) β πΏ = {π‘ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π‘β((π₯π
π¦)πΊπ§)) = ((π₯π(π‘βπ¦))π»(π‘βπ§))}) |