Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. . . 4
β’ (πΉ β LVec β πΉ β V) |
2 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΉ β (LBasisβπ) = (LBasisβπΉ)) |
3 | | dimval.1 |
. . . . . . . 8
β’ π½ = (LBasisβπΉ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΉ β (LBasisβπ) = π½) |
5 | 4 | imaeq2d 6017 |
. . . . . 6
β’ (π = πΉ β (β― β (LBasisβπ)) = (β― β π½)) |
6 | 5 | unieqd 4883 |
. . . . 5
β’ (π = πΉ β βͺ
(β― β (LBasisβπ)) = βͺ (β―
β π½)) |
7 | | df-dim 32361 |
. . . . 5
β’ dim =
(π β V β¦ βͺ (β― β (LBasisβπ))) |
8 | | hashf 14247 |
. . . . . . 7
β’
β―:VβΆ(β0 βͺ {+β}) |
9 | | ffun 6675 |
. . . . . . 7
β’
(β―:VβΆ(β0 βͺ {+β}) β Fun
β―) |
10 | 3 | fvexi 6860 |
. . . . . . . 8
β’ π½ β V |
11 | 10 | funimaex 6593 |
. . . . . . 7
β’ (Fun
β― β (β― β π½) β V) |
12 | 8, 9, 11 | mp2b 10 |
. . . . . 6
β’ (β―
β π½) β
V |
13 | 12 | uniex 7682 |
. . . . 5
β’ βͺ (β― β π½) β V |
14 | 6, 7, 13 | fvmpt 6952 |
. . . 4
β’ (πΉ β V β
(dimβπΉ) = βͺ (β― β π½)) |
15 | 1, 14 | syl 17 |
. . 3
β’ (πΉ β LVec β
(dimβπΉ) = βͺ (β― β π½)) |
16 | 15 | adantr 482 |
. 2
β’ ((πΉ β LVec β§ π β π½) β (dimβπΉ) = βͺ (β―
β π½)) |
17 | 3 | lvecdim 20663 |
. . . . . . . . . 10
β’ ((πΉ β LVec β§ π β π½ β§ π‘ β π½) β π β π‘) |
18 | 17 | ad4ant124 1174 |
. . . . . . . . 9
β’ ((((πΉ β LVec β§ π β π½) β§ π₯ β (β― β π½)) β§ π‘ β π½) β π β π‘) |
19 | | hasheni 14257 |
. . . . . . . . 9
β’ (π β π‘ β (β―βπ) = (β―βπ‘)) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
β’ ((((πΉ β LVec β§ π β π½) β§ π₯ β (β― β π½)) β§ π‘ β π½) β (β―βπ) = (β―βπ‘)) |
21 | 20 | adantr 482 |
. . . . . . 7
β’
(((((πΉ β LVec
β§ π β π½) β§ π₯ β (β― β π½)) β§ π‘ β π½) β§ (β―βπ‘) = π₯) β (β―βπ) = (β―βπ‘)) |
22 | | simpr 486 |
. . . . . . 7
β’
(((((πΉ β LVec
β§ π β π½) β§ π₯ β (β― β π½)) β§ π‘ β π½) β§ (β―βπ‘) = π₯) β (β―βπ‘) = π₯) |
23 | 21, 22 | eqtr2d 2774 |
. . . . . 6
β’
(((((πΉ β LVec
β§ π β π½) β§ π₯ β (β― β π½)) β§ π‘ β π½) β§ (β―βπ‘) = π₯) β π₯ = (β―βπ)) |
24 | 8, 9 | ax-mp 5 |
. . . . . . . 8
β’ Fun
β― |
25 | | fvelima 6912 |
. . . . . . . 8
β’ ((Fun
β― β§ π₯ β
(β― β π½)) β
βπ‘ β π½ (β―βπ‘) = π₯) |
26 | 24, 25 | mpan 689 |
. . . . . . 7
β’ (π₯ β (β― β π½) β βπ‘ β π½ (β―βπ‘) = π₯) |
27 | 26 | adantl 483 |
. . . . . 6
β’ (((πΉ β LVec β§ π β π½) β§ π₯ β (β― β π½)) β βπ‘ β π½ (β―βπ‘) = π₯) |
28 | 23, 27 | r19.29a 3156 |
. . . . 5
β’ (((πΉ β LVec β§ π β π½) β§ π₯ β (β― β π½)) β π₯ = (β―βπ)) |
29 | 28 | ralrimiva 3140 |
. . . 4
β’ ((πΉ β LVec β§ π β π½) β βπ₯ β (β― β π½)π₯ = (β―βπ)) |
30 | | ne0i 4298 |
. . . . . . 7
β’ (π β π½ β π½ β β
) |
31 | 30 | adantl 483 |
. . . . . 6
β’ ((πΉ β LVec β§ π β π½) β π½ β β
) |
32 | | ffn 6672 |
. . . . . . . . 9
β’
(β―:VβΆ(β0 βͺ {+β}) β β―
Fn V) |
33 | 8, 32 | ax-mp 5 |
. . . . . . . 8
β’ β―
Fn V |
34 | | ssv 3972 |
. . . . . . . 8
β’ π½ β V |
35 | | fnimaeq0 6638 |
. . . . . . . 8
β’ ((β―
Fn V β§ π½ β V)
β ((β― β π½)
= β
β π½ =
β
)) |
36 | 33, 34, 35 | mp2an 691 |
. . . . . . 7
β’ ((β―
β π½) = β
β
π½ =
β
) |
37 | 36 | necon3bii 2993 |
. . . . . 6
β’ ((β―
β π½) β β
β π½ β
β
) |
38 | 31, 37 | sylibr 233 |
. . . . 5
β’ ((πΉ β LVec β§ π β π½) β (β― β π½) β β
) |
39 | | eqsn 4793 |
. . . . 5
β’ ((β―
β π½) β β
β ((β― β π½)
= {(β―βπ)}
β βπ₯ β
(β― β π½)π₯ = (β―βπ))) |
40 | 38, 39 | syl 17 |
. . . 4
β’ ((πΉ β LVec β§ π β π½) β ((β― β π½) = {(β―βπ)} β βπ₯ β (β― β π½)π₯ = (β―βπ))) |
41 | 29, 40 | mpbird 257 |
. . 3
β’ ((πΉ β LVec β§ π β π½) β (β― β π½) = {(β―βπ)}) |
42 | 41 | unieqd 4883 |
. 2
β’ ((πΉ β LVec β§ π β π½) β βͺ
(β― β π½) = βͺ {(β―βπ)}) |
43 | | fvex 6859 |
. . . 4
β’
(β―βπ)
β V |
44 | 43 | unisn 4891 |
. . 3
β’ βͺ {(β―βπ)} = (β―βπ) |
45 | 44 | a1i 11 |
. 2
β’ ((πΉ β LVec β§ π β π½) β βͺ
{(β―βπ)} =
(β―βπ)) |
46 | 16, 42, 45 | 3eqtrd 2777 |
1
β’ ((πΉ β LVec β§ π β π½) β (dimβπΉ) = (β―βπ)) |