Step | Hyp | Ref
| Expression |
1 | | islssd.u |
. . . 4
β’ (π β π β π) |
2 | | islssd.v |
. . . 4
β’ (π β π = (Baseβπ)) |
3 | 1, 2 | sseqtrd 3985 |
. . 3
β’ (π β π β (Baseβπ)) |
4 | | islssd.z |
. . 3
β’ (π β π β β
) |
5 | | islssd.c |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π β π β§ π β π)) β ((π₯ Β· π) + π) β π) |
6 | 5 | 3exp2 1355 |
. . . . . . . 8
β’ (π β (π₯ β π΅ β (π β π β (π β π β ((π₯ Β· π) + π) β π)))) |
7 | 6 | imp43 429 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π β π β§ π β π)) β ((π₯ Β· π) + π) β π) |
8 | 7 | ralrimivva 3194 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β βπ β π βπ β π ((π₯ Β· π) + π) β π) |
9 | 8 | ex 414 |
. . . . 5
β’ (π β (π₯ β π΅ β βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
10 | | islssd.b |
. . . . . . 7
β’ (π β π΅ = (BaseβπΉ)) |
11 | | islssd.f |
. . . . . . . 8
β’ (π β πΉ = (Scalarβπ)) |
12 | 11 | fveq2d 6847 |
. . . . . . 7
β’ (π β (BaseβπΉ) =
(Baseβ(Scalarβπ))) |
13 | 10, 12 | eqtrd 2773 |
. . . . . 6
β’ (π β π΅ = (Baseβ(Scalarβπ))) |
14 | 13 | eleq2d 2820 |
. . . . 5
β’ (π β (π₯ β π΅ β π₯ β (Baseβ(Scalarβπ)))) |
15 | | islssd.p |
. . . . . . . . 9
β’ (π β + =
(+gβπ)) |
16 | 15 | oveqd 7375 |
. . . . . . . 8
β’ (π β ((π₯ Β· π) + π) = ((π₯ Β· π)(+gβπ)π)) |
17 | | islssd.t |
. . . . . . . . . 10
β’ (π β Β· = (
Β·π βπ)) |
18 | 17 | oveqd 7375 |
. . . . . . . . 9
β’ (π β (π₯ Β· π) = (π₯( Β·π
βπ)π)) |
19 | 18 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((π₯ Β· π)(+gβπ)π) = ((π₯( Β·π
βπ)π)(+gβπ)π)) |
20 | 16, 19 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((π₯ Β· π) + π) = ((π₯( Β·π
βπ)π)(+gβπ)π)) |
21 | 20 | eleq1d 2819 |
. . . . . 6
β’ (π β (((π₯ Β· π) + π) β π β ((π₯( Β·π
βπ)π)(+gβπ)π) β π)) |
22 | 21 | 2ralbidv 3209 |
. . . . 5
β’ (π β (βπ β π βπ β π ((π₯ Β· π) + π) β π β βπ β π βπ β π ((π₯( Β·π
βπ)π)(+gβπ)π) β π)) |
23 | 9, 14, 22 | 3imtr3d 293 |
. . . 4
β’ (π β (π₯ β (Baseβ(Scalarβπ)) β βπ β π βπ β π ((π₯( Β·π
βπ)π)(+gβπ)π) β π)) |
24 | 23 | ralrimiv 3139 |
. . 3
β’ (π β βπ₯ β (Baseβ(Scalarβπ))βπ β π βπ β π ((π₯( Β·π
βπ)π)(+gβπ)π) β π) |
25 | | eqid 2733 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
26 | | eqid 2733 |
. . . 4
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
27 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
28 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
29 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
30 | | eqid 2733 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
31 | 25, 26, 27, 28, 29, 30 | islss 20410 |
. . 3
β’ (π β (LSubSpβπ) β (π β (Baseβπ) β§ π β β
β§ βπ₯ β
(Baseβ(Scalarβπ))βπ β π βπ β π ((π₯( Β·π
βπ)π)(+gβπ)π) β π)) |
32 | 3, 4, 24, 31 | syl3anbrc 1344 |
. 2
β’ (π β π β (LSubSpβπ)) |
33 | | islssd.s |
. 2
β’ (π β π = (LSubSpβπ)) |
34 | 32, 33 | eleqtrrd 2837 |
1
β’ (π β π β π) |