Step | Hyp | Ref
| Expression |
1 | | lflset.v |
. . . 4
β’ π = (Baseβπ) |
2 | | lflset.a |
. . . 4
β’ + =
(+gβπ) |
3 | | lflset.d |
. . . 4
β’ π· = (Scalarβπ) |
4 | | lflset.s |
. . . 4
β’ Β· = (
Β·π βπ) |
5 | | lflset.k |
. . . 4
β’ πΎ = (Baseβπ·) |
6 | | lflset.p |
. . . 4
⒠⨣ =
(+gβπ·) |
7 | | lflset.t |
. . . 4
β’ Γ =
(.rβπ·) |
8 | | lflset.f |
. . . 4
β’ πΉ = (LFnlβπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | lflset 37571 |
. . 3
β’ (π β π β πΉ = {π β (πΎ βm π) β£ βπ β πΎ βπ₯ β π βπ¦ β π (πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦))}) |
10 | 9 | eleq2d 2820 |
. 2
β’ (π β π β (πΊ β πΉ β πΊ β {π β (πΎ βm π) β£ βπ β πΎ βπ₯ β π βπ¦ β π (πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦))})) |
11 | | fveq1 6845 |
. . . . . . 7
β’ (π = πΊ β (πβ((π Β· π₯) + π¦)) = (πΊβ((π Β· π₯) + π¦))) |
12 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = πΊ β (πβπ₯) = (πΊβπ₯)) |
13 | 12 | oveq2d 7377 |
. . . . . . . 8
β’ (π = πΊ β (π Γ (πβπ₯)) = (π Γ (πΊβπ₯))) |
14 | | fveq1 6845 |
. . . . . . . 8
β’ (π = πΊ β (πβπ¦) = (πΊβπ¦)) |
15 | 13, 14 | oveq12d 7379 |
. . . . . . 7
β’ (π = πΊ β ((π Γ (πβπ₯)) ⨣ (πβπ¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) |
16 | 11, 15 | eqeq12d 2749 |
. . . . . 6
β’ (π = πΊ β ((πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦)) β (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)))) |
17 | 16 | 2ralbidv 3209 |
. . . . 5
β’ (π = πΊ β (βπ₯ β π βπ¦ β π (πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦)) β βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)))) |
18 | 17 | ralbidv 3171 |
. . . 4
β’ (π = πΊ β (βπ β πΎ βπ₯ β π βπ¦ β π (πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦)) β βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)))) |
19 | 18 | elrab 3649 |
. . 3
β’ (πΊ β {π β (πΎ βm π) β£ βπ β πΎ βπ₯ β π βπ¦ β π (πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦))} β (πΊ β (πΎ βm π) β§ βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)))) |
20 | 5 | fvexi 6860 |
. . . . 5
β’ πΎ β V |
21 | 1 | fvexi 6860 |
. . . . 5
β’ π β V |
22 | 20, 21 | elmap 8815 |
. . . 4
β’ (πΊ β (πΎ βm π) β πΊ:πβΆπΎ) |
23 | 22 | anbi1i 625 |
. . 3
β’ ((πΊ β (πΎ βm π) β§ βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) β (πΊ:πβΆπΎ β§ βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)))) |
24 | 19, 23 | bitri 275 |
. 2
β’ (πΊ β {π β (πΎ βm π) β£ βπ β πΎ βπ₯ β π βπ¦ β π (πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦))} β (πΊ:πβΆπΎ β§ βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)))) |
25 | 10, 24 | bitrdi 287 |
1
β’ (π β π β (πΊ β πΉ β (πΊ:πβΆπΎ β§ βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))))) |