Step | Hyp | Ref
| Expression |
1 | | lnoval.1 |
. . . 4
β’ π = (BaseSetβπ) |
2 | | lnoval.2 |
. . . 4
β’ π = (BaseSetβπ) |
3 | | lnoval.3 |
. . . 4
β’ πΊ = ( +π£
βπ) |
4 | | lnoval.4 |
. . . 4
β’ π» = ( +π£
βπ) |
5 | | lnoval.5 |
. . . 4
β’ π
= (
Β·π OLD βπ) |
6 | | lnoval.6 |
. . . 4
β’ π = (
Β·π OLD βπ) |
7 | | lnoval.7 |
. . . 4
β’ πΏ = (π LnOp π) |
8 | 1, 2, 3, 4, 5, 6, 7 | lnoval 29736 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec) β πΏ = {π€ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π€β((π₯π
π¦)πΊπ§)) = ((π₯π(π€βπ¦))π»(π€βπ§))}) |
9 | 8 | eleq2d 2820 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec) β (π β πΏ β π β {π€ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π€β((π₯π
π¦)πΊπ§)) = ((π₯π(π€βπ¦))π»(π€βπ§))})) |
10 | | fveq1 6842 |
. . . . . . 7
β’ (π€ = π β (π€β((π₯π
π¦)πΊπ§)) = (πβ((π₯π
π¦)πΊπ§))) |
11 | | fveq1 6842 |
. . . . . . . . 9
β’ (π€ = π β (π€βπ¦) = (πβπ¦)) |
12 | 11 | oveq2d 7374 |
. . . . . . . 8
β’ (π€ = π β (π₯π(π€βπ¦)) = (π₯π(πβπ¦))) |
13 | | fveq1 6842 |
. . . . . . . 8
β’ (π€ = π β (π€βπ§) = (πβπ§)) |
14 | 12, 13 | oveq12d 7376 |
. . . . . . 7
β’ (π€ = π β ((π₯π(π€βπ¦))π»(π€βπ§)) = ((π₯π(πβπ¦))π»(πβπ§))) |
15 | 10, 14 | eqeq12d 2749 |
. . . . . 6
β’ (π€ = π β ((π€β((π₯π
π¦)πΊπ§)) = ((π₯π(π€βπ¦))π»(π€βπ§)) β (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§)))) |
16 | 15 | 2ralbidv 3209 |
. . . . 5
β’ (π€ = π β (βπ¦ β π βπ§ β π (π€β((π₯π
π¦)πΊπ§)) = ((π₯π(π€βπ¦))π»(π€βπ§)) β βπ¦ β π βπ§ β π (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§)))) |
17 | 16 | ralbidv 3171 |
. . . 4
β’ (π€ = π β (βπ₯ β β βπ¦ β π βπ§ β π (π€β((π₯π
π¦)πΊπ§)) = ((π₯π(π€βπ¦))π»(π€βπ§)) β βπ₯ β β βπ¦ β π βπ§ β π (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§)))) |
18 | 17 | elrab 3646 |
. . 3
β’ (π β {π€ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π€β((π₯π
π¦)πΊπ§)) = ((π₯π(π€βπ¦))π»(π€βπ§))} β (π β (π βm π) β§ βπ₯ β β βπ¦ β π βπ§ β π (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§)))) |
19 | 2 | fvexi 6857 |
. . . . 5
β’ π β V |
20 | 1 | fvexi 6857 |
. . . . 5
β’ π β V |
21 | 19, 20 | elmap 8812 |
. . . 4
β’ (π β (π βm π) β π:πβΆπ) |
22 | 21 | anbi1i 625 |
. . 3
β’ ((π β (π βm π) β§ βπ₯ β β βπ¦ β π βπ§ β π (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§))) β (π:πβΆπ β§ βπ₯ β β βπ¦ β π βπ§ β π (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§)))) |
23 | 18, 22 | bitri 275 |
. 2
β’ (π β {π€ β (π βm π) β£ βπ₯ β β βπ¦ β π βπ§ β π (π€β((π₯π
π¦)πΊπ§)) = ((π₯π(π€βπ¦))π»(π€βπ§))} β (π:πβΆπ β§ βπ₯ β β βπ¦ β π βπ§ β π (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§)))) |
24 | 9, 23 | bitrdi 287 |
1
β’ ((π β NrmCVec β§ π β NrmCVec) β (π β πΏ β (π:πβΆπ β§ βπ₯ β β βπ¦ β π βπ§ β π (πβ((π₯π
π¦)πΊπ§)) = ((π₯π(πβπ¦))π»(πβπ§))))) |