Step | Hyp | Ref
| Expression |
1 | | lindfpropd.2 |
. . . . . . . 8
β’ (π β
(Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΏ))) |
2 | | lindfpropd.3 |
. . . . . . . . 9
β’ (π β
(0gβ(ScalarβπΎ)) =
(0gβ(ScalarβπΏ))) |
3 | 2 | sneqd 4599 |
. . . . . . . 8
β’ (π β
{(0gβ(ScalarβπΎ))} =
{(0gβ(ScalarβπΏ))}) |
4 | 1, 3 | difeq12d 4084 |
. . . . . . 7
β’ (π β
((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) = ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))})) |
5 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) = ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))})) |
6 | | simplll 774 |
. . . . . . . . 9
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β π) |
7 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) |
8 | 7 | eldifad 3923 |
. . . . . . . . 9
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β π β (Baseβ(ScalarβπΎ))) |
9 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π:dom πβΆ(BaseβπΎ)) β π:dom πβΆ(BaseβπΎ)) |
10 | 9 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β (πβπ) β (BaseβπΎ)) |
11 | 10 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β (πβπ) β (BaseβπΎ)) |
12 | | lindfpropd.6 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) |
13 | 12 | oveqrspc2v 7385 |
. . . . . . . . 9
β’ ((π β§ (π β (Baseβ(ScalarβπΎ)) β§ (πβπ) β (BaseβπΎ))) β (π( Β·π
βπΎ)(πβπ)) = (π( Β·π
βπΏ)(πβπ))) |
14 | 6, 8, 11, 13 | syl12anc 836 |
. . . . . . . 8
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β (π( Β·π
βπΎ)(πβπ)) = (π( Β·π
βπΏ)(πβπ))) |
15 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π β (BaseβπΎ) = (BaseβπΎ)) |
16 | | lindfpropd.1 |
. . . . . . . . . . 11
β’ (π β (BaseβπΎ) = (BaseβπΏ)) |
17 | | ssidd 3968 |
. . . . . . . . . . 11
β’ (π β (BaseβπΎ) β (BaseβπΎ)) |
18 | | lindfpropd.4 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ))) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) |
19 | | lindfpropd.5 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π
βπΎ)π¦) β (BaseβπΎ)) |
20 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π β
(Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΎ))) |
21 | | lindfpropd.k |
. . . . . . . . . . 11
β’ (π β πΎ β π) |
22 | | lindfpropd.l |
. . . . . . . . . . 11
β’ (π β πΏ β π) |
23 | 15, 16, 17, 18, 19, 12, 20, 1, 21, 22 | lsppropd 20494 |
. . . . . . . . . 10
β’ (π β (LSpanβπΎ) = (LSpanβπΏ)) |
24 | 23 | fveq1d 6845 |
. . . . . . . . 9
β’ (π β ((LSpanβπΎ)β(π β (dom π β {π}))) = ((LSpanβπΏ)β(π β (dom π β {π})))) |
25 | 24 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β ((LSpanβπΎ)β(π β (dom π β {π}))) = ((LSpanβπΏ)β(π β (dom π β {π})))) |
26 | 14, 25 | eleq12d 2828 |
. . . . . . 7
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β ((π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π}))) β (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π}))))) |
27 | 26 | notbid 318 |
. . . . . 6
β’ ((((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β§ π β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))})) β (Β¬ (π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π}))) β Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π}))))) |
28 | 5, 27 | raleqbidva 3320 |
. . . . 5
β’ (((π β§ π:dom πβΆ(BaseβπΎ)) β§ π β dom π) β (βπ β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) Β¬ (π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π}))) β βπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π}))))) |
29 | 28 | ralbidva 3169 |
. . . 4
β’ ((π β§ π:dom πβΆ(BaseβπΎ)) β (βπ β dom πβπ β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) Β¬ (π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π}))) β βπ β dom πβπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π}))))) |
30 | 29 | pm5.32da 580 |
. . 3
β’ (π β ((π:dom πβΆ(BaseβπΎ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) Β¬ (π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π})))) β (π:dom πβΆ(BaseβπΎ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π})))))) |
31 | 16 | feq3d 6656 |
. . . 4
β’ (π β (π:dom πβΆ(BaseβπΎ) β π:dom πβΆ(BaseβπΏ))) |
32 | 31 | anbi1d 631 |
. . 3
β’ (π β ((π:dom πβΆ(BaseβπΎ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π})))) β (π:dom πβΆ(BaseβπΏ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π})))))) |
33 | 30, 32 | bitrd 279 |
. 2
β’ (π β ((π:dom πβΆ(BaseβπΎ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) Β¬ (π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π})))) β (π:dom πβΆ(BaseβπΏ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π})))))) |
34 | | lindfpropd.x |
. . 3
β’ (π β π β π΄) |
35 | | eqid 2733 |
. . . 4
β’
(BaseβπΎ) =
(BaseβπΎ) |
36 | | eqid 2733 |
. . . 4
β’ (
Β·π βπΎ) = ( Β·π
βπΎ) |
37 | | eqid 2733 |
. . . 4
β’
(LSpanβπΎ) =
(LSpanβπΎ) |
38 | | eqid 2733 |
. . . 4
β’
(ScalarβπΎ) =
(ScalarβπΎ) |
39 | | eqid 2733 |
. . . 4
β’
(Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΎ)) |
40 | | eqid 2733 |
. . . 4
β’
(0gβ(ScalarβπΎ)) =
(0gβ(ScalarβπΎ)) |
41 | 35, 36, 37, 38, 39, 40 | islindf 21234 |
. . 3
β’ ((πΎ β π β§ π β π΄) β (π LIndF πΎ β (π:dom πβΆ(BaseβπΎ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) Β¬ (π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π})))))) |
42 | 21, 34, 41 | syl2anc 585 |
. 2
β’ (π β (π LIndF πΎ β (π:dom πβΆ(BaseβπΎ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΎ)) β
{(0gβ(ScalarβπΎ))}) Β¬ (π( Β·π
βπΎ)(πβπ)) β ((LSpanβπΎ)β(π β (dom π β {π})))))) |
43 | | eqid 2733 |
. . . 4
β’
(BaseβπΏ) =
(BaseβπΏ) |
44 | | eqid 2733 |
. . . 4
β’ (
Β·π βπΏ) = ( Β·π
βπΏ) |
45 | | eqid 2733 |
. . . 4
β’
(LSpanβπΏ) =
(LSpanβπΏ) |
46 | | eqid 2733 |
. . . 4
β’
(ScalarβπΏ) =
(ScalarβπΏ) |
47 | | eqid 2733 |
. . . 4
β’
(Baseβ(ScalarβπΏ)) = (Baseβ(ScalarβπΏ)) |
48 | | eqid 2733 |
. . . 4
β’
(0gβ(ScalarβπΏ)) =
(0gβ(ScalarβπΏ)) |
49 | 43, 44, 45, 46, 47, 48 | islindf 21234 |
. . 3
β’ ((πΏ β π β§ π β π΄) β (π LIndF πΏ β (π:dom πβΆ(BaseβπΏ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π})))))) |
50 | 22, 34, 49 | syl2anc 585 |
. 2
β’ (π β (π LIndF πΏ β (π:dom πβΆ(BaseβπΏ) β§ βπ β dom πβπ β ((Baseβ(ScalarβπΏ)) β
{(0gβ(ScalarβπΏ))}) Β¬ (π( Β·π
βπΏ)(πβπ)) β ((LSpanβπΏ)β(π β (dom π β {π})))))) |
51 | 33, 42, 50 | 3bitr4d 311 |
1
β’ (π β (π LIndF πΎ β π LIndF πΏ)) |