Step | Hyp | Ref
| Expression |
1 | | feq1 6650 |
. . . . . 6
β’ (π = πΉ β (π:dom πβΆ(Baseβπ€) β πΉ:dom πβΆ(Baseβπ€))) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π = πΉ β§ π€ = π) β (π:dom πβΆ(Baseβπ€) β πΉ:dom πβΆ(Baseβπ€))) |
3 | | dmeq 5860 |
. . . . . . 7
β’ (π = πΉ β dom π = dom πΉ) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π = πΉ β§ π€ = π) β dom π = dom πΉ) |
5 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
6 | | islindf.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β (Baseβπ€) = π΅) |
8 | 7 | adantl 483 |
. . . . . 6
β’ ((π = πΉ β§ π€ = π) β (Baseβπ€) = π΅) |
9 | 4, 8 | feq23d 6664 |
. . . . 5
β’ ((π = πΉ β§ π€ = π) β (πΉ:dom πβΆ(Baseβπ€) β πΉ:dom πΉβΆπ΅)) |
10 | 2, 9 | bitrd 279 |
. . . 4
β’ ((π = πΉ β§ π€ = π) β (π:dom πβΆ(Baseβπ€) β πΉ:dom πΉβΆπ΅)) |
11 | | fvex 6856 |
. . . . . 6
β’
(Scalarβπ€)
β V |
12 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (Scalarβπ€) β (Baseβπ ) =
(Baseβ(Scalarβπ€))) |
13 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = (Scalarβπ€) β
(0gβπ ) =
(0gβ(Scalarβπ€))) |
14 | 13 | sneqd 4599 |
. . . . . . . . 9
β’ (π = (Scalarβπ€) β
{(0gβπ )} =
{(0gβ(Scalarβπ€))}) |
15 | 12, 14 | difeq12d 4084 |
. . . . . . . 8
β’ (π = (Scalarβπ€) β ((Baseβπ ) β
{(0gβπ )})
= ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))})) |
16 | 15 | raleqdv 3312 |
. . . . . . 7
β’ (π = (Scalarβπ€) β (βπ β ((Baseβπ ) β
{(0gβπ )})
Β¬ (π(
Β·π βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β βπ β ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))))) |
17 | 16 | ralbidv 3171 |
. . . . . 6
β’ (π = (Scalarβπ€) β (βπ₯ β dom πβπ β ((Baseβπ ) β {(0gβπ )}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β βπ₯ β dom πβπ β ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))))) |
18 | 11, 17 | sbcie 3783 |
. . . . 5
β’
([(Scalarβπ€) / π ]βπ₯ β dom πβπ β ((Baseβπ ) β {(0gβπ )}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β βπ₯ β dom πβπ β ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯})))) |
19 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π€ = π β (Scalarβπ€) = (Scalarβπ)) |
20 | | islindf.s |
. . . . . . . . . . . 12
β’ π = (Scalarβπ) |
21 | 19, 20 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π€ = π β (Scalarβπ€) = π) |
22 | 21 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π€ = π β (Baseβ(Scalarβπ€)) = (Baseβπ)) |
23 | | islindf.n |
. . . . . . . . . 10
β’ π = (Baseβπ) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π€ = π β (Baseβ(Scalarβπ€)) = π) |
25 | 21 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π€ = π β
(0gβ(Scalarβπ€)) = (0gβπ)) |
26 | | islindf.z |
. . . . . . . . . . 11
β’ 0 =
(0gβπ) |
27 | 25, 26 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π€ = π β
(0gβ(Scalarβπ€)) = 0 ) |
28 | 27 | sneqd 4599 |
. . . . . . . . 9
β’ (π€ = π β
{(0gβ(Scalarβπ€))} = { 0 }) |
29 | 24, 28 | difeq12d 4084 |
. . . . . . . 8
β’ (π€ = π β ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))}) = (π β { 0 })) |
30 | 29 | adantl 483 |
. . . . . . 7
β’ ((π = πΉ β§ π€ = π) β ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))}) = (π β { 0 })) |
31 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π€ = π β (
Β·π βπ€) = ( Β·π
βπ)) |
32 | | islindf.v |
. . . . . . . . . . . 12
β’ Β· = (
Β·π βπ) |
33 | 31, 32 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π€ = π β (
Β·π βπ€) = Β· ) |
34 | 33 | adantl 483 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π€ = π) β (
Β·π βπ€) = Β· ) |
35 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π€ = π) β π = π) |
36 | | fveq1 6842 |
. . . . . . . . . . 11
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
37 | 36 | adantr 482 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π€ = π) β (πβπ₯) = (πΉβπ₯)) |
38 | 34, 35, 37 | oveq123d 7379 |
. . . . . . . . 9
β’ ((π = πΉ β§ π€ = π) β (π( Β·π
βπ€)(πβπ₯)) = (π Β· (πΉβπ₯))) |
39 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π€ = π β (LSpanβπ€) = (LSpanβπ)) |
40 | | islindf.k |
. . . . . . . . . . . 12
β’ πΎ = (LSpanβπ) |
41 | 39, 40 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π€ = π β (LSpanβπ€) = πΎ) |
42 | 41 | adantl 483 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π€ = π) β (LSpanβπ€) = πΎ) |
43 | | imaeq1 6009 |
. . . . . . . . . . . 12
β’ (π = πΉ β (π β (dom π β {π₯})) = (πΉ β (dom π β {π₯}))) |
44 | 3 | difeq1d 4082 |
. . . . . . . . . . . . 13
β’ (π = πΉ β (dom π β {π₯}) = (dom πΉ β {π₯})) |
45 | 44 | imaeq2d 6014 |
. . . . . . . . . . . 12
β’ (π = πΉ β (πΉ β (dom π β {π₯})) = (πΉ β (dom πΉ β {π₯}))) |
46 | 43, 45 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π = πΉ β (π β (dom π β {π₯})) = (πΉ β (dom πΉ β {π₯}))) |
47 | 46 | adantr 482 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π€ = π) β (π β (dom π β {π₯})) = (πΉ β (dom πΉ β {π₯}))) |
48 | 42, 47 | fveq12d 6850 |
. . . . . . . . 9
β’ ((π = πΉ β§ π€ = π) β ((LSpanβπ€)β(π β (dom π β {π₯}))) = (πΎβ(πΉ β (dom πΉ β {π₯})))) |
49 | 38, 48 | eleq12d 2828 |
. . . . . . . 8
β’ ((π = πΉ β§ π€ = π) β ((π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))))) |
50 | 49 | notbid 318 |
. . . . . . 7
β’ ((π = πΉ β§ π€ = π) β (Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))))) |
51 | 30, 50 | raleqbidv 3318 |
. . . . . 6
β’ ((π = πΉ β§ π€ = π) β (βπ β ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β βπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))))) |
52 | 4, 51 | raleqbidv 3318 |
. . . . 5
β’ ((π = πΉ β§ π€ = π) β (βπ₯ β dom πβπ β ((Baseβ(Scalarβπ€)) β
{(0gβ(Scalarβπ€))}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))))) |
53 | 18, 52 | bitrid 283 |
. . . 4
β’ ((π = πΉ β§ π€ = π) β ([(Scalarβπ€) / π ]βπ₯ β dom πβπ β ((Baseβπ ) β {(0gβπ )}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))) β βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))))) |
54 | 10, 53 | anbi12d 632 |
. . 3
β’ ((π = πΉ β§ π€ = π) β ((π:dom πβΆ(Baseβπ€) β§ [(Scalarβπ€) / π ]βπ₯ β dom πβπ β ((Baseβπ ) β {(0gβπ )}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯})))) β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯})))))) |
55 | | df-lindf 21228 |
. . 3
β’ LIndF =
{β¨π, π€β© β£ (π:dom πβΆ(Baseβπ€) β§ [(Scalarβπ€) / π ]βπ₯ β dom πβπ β ((Baseβπ ) β {(0gβπ )}) Β¬ (π( Β·π
βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))))} |
56 | 54, 55 | brabga 5492 |
. 2
β’ ((πΉ β π β§ π β π) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯})))))) |
57 | 56 | ancoms 460 |
1
β’ ((π β π β§ πΉ β π) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯})))))) |