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 | 3ad2ant1 1134 |
. 2
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β (dimβπΉ) = βͺ
(β― β π½)) |
17 | | simpll1 1213 |
. . . . . . . . . 10
β’ ((((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β πΉ β LVec) |
18 | | simpll2 1214 |
. . . . . . . . . 10
β’ ((((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β π β π½) |
19 | | simpr 486 |
. . . . . . . . . 10
β’ ((((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β π‘ β π½) |
20 | | simpll3 1215 |
. . . . . . . . . 10
β’ ((((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β π β Fin) |
21 | 3, 17, 18, 19, 20 | lvecdimfi 32359 |
. . . . . . . . 9
β’ ((((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β π β π‘) |
22 | | hasheni 14257 |
. . . . . . . . 9
β’ (π β π‘ β (β―βπ) = (β―βπ‘)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
β’ ((((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β (β―βπ) = (β―βπ‘)) |
24 | 23 | adantr 482 |
. . . . . . 7
β’
(((((πΉ β LVec
β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β§ (β―βπ‘) = π₯) β (β―βπ) = (β―βπ‘)) |
25 | | simpr 486 |
. . . . . . 7
β’
(((((πΉ β LVec
β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β§ (β―βπ‘) = π₯) β (β―βπ‘) = π₯) |
26 | 24, 25 | eqtr2d 2774 |
. . . . . 6
β’
(((((πΉ β LVec
β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β§ π‘ β π½) β§ (β―βπ‘) = π₯) β π₯ = (β―βπ)) |
27 | 8, 9 | ax-mp 5 |
. . . . . . . 8
β’ Fun
β― |
28 | | fvelima 6912 |
. . . . . . . 8
β’ ((Fun
β― β§ π₯ β
(β― β π½)) β
βπ‘ β π½ (β―βπ‘) = π₯) |
29 | 27, 28 | mpan 689 |
. . . . . . 7
β’ (π₯ β (β― β π½) β βπ‘ β π½ (β―βπ‘) = π₯) |
30 | 29 | adantl 483 |
. . . . . 6
β’ (((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β βπ‘ β π½ (β―βπ‘) = π₯) |
31 | 26, 30 | r19.29a 3156 |
. . . . 5
β’ (((πΉ β LVec β§ π β π½ β§ π β Fin) β§ π₯ β (β― β π½)) β π₯ = (β―βπ)) |
32 | 31 | ralrimiva 3140 |
. . . 4
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β βπ₯ β (β― β π½)π₯ = (β―βπ)) |
33 | | ne0i 4298 |
. . . . . . 7
β’ (π β π½ β π½ β β
) |
34 | 33 | 3ad2ant2 1135 |
. . . . . 6
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β π½ β β
) |
35 | | ffn 6672 |
. . . . . . . . 9
β’
(β―:VβΆ(β0 βͺ {+β}) β β―
Fn V) |
36 | 8, 35 | ax-mp 5 |
. . . . . . . 8
β’ β―
Fn V |
37 | | ssv 3972 |
. . . . . . . 8
β’ π½ β V |
38 | | fnimaeq0 6638 |
. . . . . . . 8
β’ ((β―
Fn V β§ π½ β V)
β ((β― β π½)
= β
β π½ =
β
)) |
39 | 36, 37, 38 | mp2an 691 |
. . . . . . 7
β’ ((β―
β π½) = β
β
π½ =
β
) |
40 | 39 | necon3bii 2993 |
. . . . . 6
β’ ((β―
β π½) β β
β π½ β
β
) |
41 | 34, 40 | sylibr 233 |
. . . . 5
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β (β― β π½) β β
) |
42 | | eqsn 4793 |
. . . . 5
β’ ((β―
β π½) β β
β ((β― β π½)
= {(β―βπ)}
β βπ₯ β
(β― β π½)π₯ = (β―βπ))) |
43 | 41, 42 | syl 17 |
. . . 4
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β ((β― β π½) = {(β―βπ)} β βπ₯ β (β― β π½)π₯ = (β―βπ))) |
44 | 32, 43 | mpbird 257 |
. . 3
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β (β― β π½) = {(β―βπ)}) |
45 | 44 | unieqd 4883 |
. 2
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β βͺ (β― β π½) = βͺ
{(β―βπ)}) |
46 | | fvex 6859 |
. . . 4
β’
(β―βπ)
β V |
47 | 46 | unisn 4891 |
. . 3
β’ βͺ {(β―βπ)} = (β―βπ) |
48 | 47 | a1i 11 |
. 2
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β βͺ {(β―βπ)} = (β―βπ)) |
49 | 16, 45, 48 | 3eqtrd 2777 |
1
β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β (dimβπΉ) = (β―βπ)) |