Step | Hyp | Ref
| Expression |
1 | | dochfl1.x |
. . . 4
β’ (π β π β (π β { 0 })) |
2 | 1 | eldifad 3959 |
. . 3
β’ (π β π β π) |
3 | | eqeq1 2736 |
. . . . . 6
β’ (π£ = π β (π£ = (π€ + (π Β· π)) β π = (π€ + (π Β· π)))) |
4 | 3 | rexbidv 3178 |
. . . . 5
β’ (π£ = π β (βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π)) β βπ€ β ( β₯ β{π})π = (π€ + (π Β· π)))) |
5 | 4 | riotabidv 7363 |
. . . 4
β’ (π£ = π β (β©π β π
βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π))) = (β©π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π)))) |
6 | | dochfl1.g |
. . . 4
β’ πΊ = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π)))) |
7 | | riotaex 7365 |
. . . 4
β’
(β©π
β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π))) β V |
8 | 5, 6, 7 | fvmpt 6995 |
. . 3
β’ (π β π β (πΊβπ) = (β©π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π)))) |
9 | 2, 8 | syl 17 |
. 2
β’ (π β (πΊβπ) = (β©π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π)))) |
10 | | dochfl1.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
11 | | dochfl1.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
12 | | dochfl1.k |
. . . . . 6
β’ (π β (πΎ β HL β§ π β π»)) |
13 | 10, 11, 12 | dvhlmod 39969 |
. . . . 5
β’ (π β π β LMod) |
14 | 2 | snssd 4811 |
. . . . . 6
β’ (π β {π} β π) |
15 | | dochfl1.v |
. . . . . . 7
β’ π = (Baseβπ) |
16 | | eqid 2732 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
17 | | dochfl1.o |
. . . . . . 7
β’ β₯ =
((ocHβπΎ)βπ) |
18 | 10, 11, 15, 16, 17 | dochlss 40213 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ {π} β π) β ( β₯ β{π}) β (LSubSpβπ)) |
19 | 12, 14, 18 | syl2anc 584 |
. . . . 5
β’ (π β ( β₯ β{π}) β (LSubSpβπ)) |
20 | | dochfl1.z |
. . . . . 6
β’ 0 =
(0gβπ) |
21 | 20, 16 | lss0cl 20549 |
. . . . 5
β’ ((π β LMod β§ ( β₯
β{π}) β
(LSubSpβπ)) β
0 β
( β₯
β{π})) |
22 | 13, 19, 21 | syl2anc 584 |
. . . 4
β’ (π β 0 β ( β₯
β{π})) |
23 | | dochfl1.d |
. . . . . . . 8
β’ π· = (Scalarβπ) |
24 | | dochfl1.t |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
25 | | dochfl1.i |
. . . . . . . 8
β’ 1 =
(1rβπ·) |
26 | 15, 23, 24, 25 | lmodvs1 20492 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β ( 1 Β· π) = π) |
27 | 13, 2, 26 | syl2anc 584 |
. . . . . 6
β’ (π β ( 1 Β· π) = π) |
28 | 27 | oveq2d 7421 |
. . . . 5
β’ (π β ( 0 + ( 1 Β· π)) = ( 0 + π)) |
29 | | dochfl1.a |
. . . . . . 7
β’ + =
(+gβπ) |
30 | 15, 29, 20 | lmod0vlid 20494 |
. . . . . 6
β’ ((π β LMod β§ π β π) β ( 0 + π) = π) |
31 | 13, 2, 30 | syl2anc 584 |
. . . . 5
β’ (π β ( 0 + π) = π) |
32 | 28, 31 | eqtr2d 2773 |
. . . 4
β’ (π β π = ( 0 + ( 1 Β· π))) |
33 | | oveq1 7412 |
. . . . 5
β’ (π€ = 0 β (π€ + ( 1 Β· π)) = ( 0 + ( 1 Β· π))) |
34 | 33 | rspceeqv 3632 |
. . . 4
β’ (( 0 β (
β₯
β{π}) β§ π = ( 0 + ( 1 Β· π))) β βπ€ β ( β₯ β{π})π = (π€ + ( 1 Β· π))) |
35 | 22, 32, 34 | syl2anc 584 |
. . 3
β’ (π β βπ€ β ( β₯ β{π})π = (π€ + ( 1 Β· π))) |
36 | 23 | lmodring 20471 |
. . . . 5
β’ (π β LMod β π· β Ring) |
37 | | dochfl1.r |
. . . . . 6
β’ π
= (Baseβπ·) |
38 | 37, 25 | ringidcl 20076 |
. . . . 5
β’ (π· β Ring β 1 β π
) |
39 | 13, 36, 38 | 3syl 18 |
. . . 4
β’ (π β 1 β π
) |
40 | | eqid 2732 |
. . . . 5
β’
(LSpanβπ) =
(LSpanβπ) |
41 | | eqid 2732 |
. . . . 5
β’
(LSSumβπ) =
(LSSumβπ) |
42 | | eqid 2732 |
. . . . 5
β’
(LSHypβπ) =
(LSHypβπ) |
43 | 10, 11, 12 | dvhlvec 39968 |
. . . . 5
β’ (π β π β LVec) |
44 | 10, 17, 11, 15, 20, 42, 12, 1 | dochsnshp 40312 |
. . . . 5
β’ (π β ( β₯ β{π}) β (LSHypβπ)) |
45 | 10, 17, 11, 15, 20, 40, 41, 12, 1 | dochexmidat 40318 |
. . . . 5
β’ (π β (( β₯ β{π})(LSSumβπ)((LSpanβπ)β{π})) = π) |
46 | 15, 29, 40, 41, 42, 43, 44, 2, 2, 45, 23, 37, 24 | lshpsmreu 37967 |
. . . 4
β’ (π β β!π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π))) |
47 | | oveq1 7412 |
. . . . . . . 8
β’ (π = 1 β (π Β· π) = ( 1 Β· π)) |
48 | 47 | oveq2d 7421 |
. . . . . . 7
β’ (π = 1 β (π€ + (π Β· π)) = (π€ + ( 1 Β· π))) |
49 | 48 | eqeq2d 2743 |
. . . . . 6
β’ (π = 1 β (π = (π€ + (π Β· π)) β π = (π€ + ( 1 Β· π)))) |
50 | 49 | rexbidv 3178 |
. . . . 5
β’ (π = 1 β (βπ€ β ( β₯ β{π})π = (π€ + (π Β· π)) β βπ€ β ( β₯ β{π})π = (π€ + ( 1 Β· π)))) |
51 | 50 | riota2 7387 |
. . . 4
β’ (( 1 β π
β§ β!π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π))) β (βπ€ β ( β₯ β{π})π = (π€ + ( 1 Β· π)) β (β©π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π))) = 1 )) |
52 | 39, 46, 51 | syl2anc 584 |
. . 3
β’ (π β (βπ€ β ( β₯ β{π})π = (π€ + ( 1 Β· π)) β (β©π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π))) = 1 )) |
53 | 35, 52 | mpbid 231 |
. 2
β’ (π β (β©π β π
βπ€ β ( β₯ β{π})π = (π€ + (π Β· π))) = 1 ) |
54 | 9, 53 | eqtrd 2772 |
1
β’ (π β (πΊβπ) = 1 ) |