Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((πΉ LIndF π β§ π β π) β πΉ LIndF π) |
2 | | rellindf 21230 |
. . . . . 6
β’ Rel
LIndF |
3 | 2 | brrelex1i 5689 |
. . . . 5
β’ (πΉ LIndF π β πΉ β V) |
4 | | lindff.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
5 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
6 | | eqid 2733 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
7 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
8 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
9 | | eqid 2733 |
. . . . . 6
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
10 | 4, 5, 6, 7, 8, 9 | islindf 21234 |
. . . . 5
β’ ((π β π β§ πΉ β V) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (dom πΉ β {π₯})))))) |
11 | 3, 10 | sylan2 594 |
. . . 4
β’ ((π β π β§ πΉ LIndF π) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (dom πΉ β {π₯})))))) |
12 | 11 | ancoms 460 |
. . 3
β’ ((πΉ LIndF π β§ π β π) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (dom πΉ β {π₯})))))) |
13 | 1, 12 | mpbid 231 |
. 2
β’ ((πΉ LIndF π β§ π β π) β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (dom πΉ β {π₯}))))) |
14 | 13 | simpld 496 |
1
β’ ((πΉ LIndF π β§ π β π) β πΉ:dom πΉβΆπ΅) |