Step | Hyp | Ref
| Expression |
1 | | islfld.w |
. . 3
β’ (π β π β π) |
2 | | islfld.u |
. . . 4
β’ (π β πΊ:πβΆπΎ) |
3 | | islfld.v |
. . . . 5
β’ (π β π = (Baseβπ)) |
4 | | islfld.k |
. . . . . 6
β’ (π β πΎ = (Baseβπ·)) |
5 | | islfld.d |
. . . . . . 7
β’ (π β π· = (Scalarβπ)) |
6 | 5 | fveq2d 6896 |
. . . . . 6
β’ (π β (Baseβπ·) =
(Baseβ(Scalarβπ))) |
7 | 4, 6 | eqtrd 2773 |
. . . . 5
β’ (π β πΎ = (Baseβ(Scalarβπ))) |
8 | 3, 7 | feq23d 6713 |
. . . 4
β’ (π β (πΊ:πβΆπΎ β πΊ:(Baseβπ)βΆ(Baseβ(Scalarβπ)))) |
9 | 2, 8 | mpbid 231 |
. . 3
β’ (π β πΊ:(Baseβπ)βΆ(Baseβ(Scalarβπ))) |
10 | | islfld.l |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) |
11 | 10 | ralrimivvva 3204 |
. . . 4
β’ (π β βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) |
12 | | islfld.a |
. . . . . . . . . 10
β’ (π β + =
(+gβπ)) |
13 | | islfld.s |
. . . . . . . . . . 11
β’ (π β Β· = (
Β·π βπ)) |
14 | 13 | oveqd 7426 |
. . . . . . . . . 10
β’ (π β (π Β· π₯) = (π( Β·π
βπ)π₯)) |
15 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π β π¦ = π¦) |
16 | 12, 14, 15 | oveq123d 7430 |
. . . . . . . . 9
β’ (π β ((π Β· π₯) + π¦) = ((π( Β·π
βπ)π₯)(+gβπ)π¦)) |
17 | 16 | fveq2d 6896 |
. . . . . . . 8
β’ (π β (πΊβ((π Β· π₯) + π¦)) = (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦))) |
18 | | islfld.p |
. . . . . . . . . 10
β’ (π β ⨣ =
(+gβπ·)) |
19 | 5 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π β (+gβπ·) =
(+gβ(Scalarβπ))) |
20 | 18, 19 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ⨣ =
(+gβ(Scalarβπ))) |
21 | | islfld.t |
. . . . . . . . . . 11
β’ (π β Γ =
(.rβπ·)) |
22 | 5 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π β (.rβπ·) =
(.rβ(Scalarβπ))) |
23 | 21, 22 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β Γ =
(.rβ(Scalarβπ))) |
24 | 23 | oveqd 7426 |
. . . . . . . . 9
β’ (π β (π Γ (πΊβπ₯)) = (π(.rβ(Scalarβπ))(πΊβπ₯))) |
25 | | eqidd 2734 |
. . . . . . . . 9
β’ (π β (πΊβπ¦) = (πΊβπ¦)) |
26 | 20, 24, 25 | oveq123d 7430 |
. . . . . . . 8
β’ (π β ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦))) |
27 | 17, 26 | eqeq12d 2749 |
. . . . . . 7
β’ (π β ((πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦)))) |
28 | 3, 27 | raleqbidv 3343 |
. . . . . 6
β’ (π β (βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β βπ¦ β (Baseβπ)(πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦)))) |
29 | 3, 28 | raleqbidv 3343 |
. . . . 5
β’ (π β (βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦)))) |
30 | 7, 29 | raleqbidv 3343 |
. . . 4
β’ (π β (βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β βπ β (Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦)))) |
31 | 11, 30 | mpbid 231 |
. . 3
β’ (π β βπ β (Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦))) |
32 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
33 | | eqid 2733 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
34 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
35 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπ) = ( Β·π
βπ) |
36 | | eqid 2733 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
37 | | eqid 2733 |
. . . . 5
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
38 | | eqid 2733 |
. . . . 5
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
39 | | eqid 2733 |
. . . . 5
β’
(LFnlβπ) =
(LFnlβπ) |
40 | 32, 33, 34, 35, 36, 37, 38, 39 | islfl 37978 |
. . . 4
β’ (π β π β (πΊ β (LFnlβπ) β (πΊ:(Baseβπ)βΆ(Baseβ(Scalarβπ)) β§ βπ β
(Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦))))) |
41 | 40 | biimpar 479 |
. . 3
β’ ((π β π β§ (πΊ:(Baseβπ)βΆ(Baseβ(Scalarβπ)) β§ βπ β
(Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦)))) β πΊ β (LFnlβπ)) |
42 | 1, 9, 31, 41 | syl12anc 836 |
. 2
β’ (π β πΊ β (LFnlβπ)) |
43 | | islfld.f |
. 2
β’ (π β πΉ = (LFnlβπ)) |
44 | 42, 43 | eleqtrrd 2837 |
1
β’ (π β πΊ β πΉ) |