Step | Hyp | Ref
| Expression |
1 | | lcfl7lem.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | lcfl7lem.o |
. . . . . 6
β’ β₯ =
((ocHβπΎ)βπ) |
3 | | lcfl7lem.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
4 | | lcfl7lem.v |
. . . . . 6
β’ π = (Baseβπ) |
5 | | lcfl7lem.z |
. . . . . 6
β’ 0 =
(0gβπ) |
6 | | lcfl7lem.a |
. . . . . 6
β’ + =
(+gβπ) |
7 | | lcfl7lem.t |
. . . . . 6
β’ Β· = (
Β·π βπ) |
8 | | lcfl7lem.l |
. . . . . 6
β’ πΏ = (LKerβπ) |
9 | | lcfl7lem.s |
. . . . . 6
β’ π = (Scalarβπ) |
10 | | lcfl7lem.r |
. . . . . 6
β’ π
= (Baseβπ) |
11 | | lcfl7lem.g |
. . . . . 6
β’ πΊ = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π)))) |
12 | | lcfl7lem.k |
. . . . . 6
β’ (π β (πΎ β HL β§ π β π»)) |
13 | | lcfl7lem.x |
. . . . . 6
β’ (π β π β (π β { 0 })) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | dochsnkr2cl 40333 |
. . . . 5
β’ (π β π β (( β₯ β(πΏβπΊ)) β { 0 })) |
15 | 14 | eldifad 3959 |
. . . 4
β’ (π β π β ( β₯ β(πΏβπΊ))) |
16 | | lcfl7lem.gj |
. . . . . . . 8
β’ (π β πΊ = π½) |
17 | 16 | fveq2d 6892 |
. . . . . . 7
β’ (π β (πΏβπΊ) = (πΏβπ½)) |
18 | | lcfl7lem.j |
. . . . . . . 8
β’ π½ = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π)))) |
19 | | lcfl7lem.x2 |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
18, 12, 19 | dochsnkr2 40332 |
. . . . . . 7
β’ (π β (πΏβπ½) = ( β₯ β{π})) |
21 | 17, 20 | eqtrd 2772 |
. . . . . 6
β’ (π β (πΏβπΊ) = ( β₯ β{π})) |
22 | 21 | fveq2d 6892 |
. . . . 5
β’ (π β ( β₯ β(πΏβπΊ)) = ( β₯ β( β₯
β{π}))) |
23 | | eqid 2732 |
. . . . . . 7
β’
(LSpanβπ) =
(LSpanβπ) |
24 | 19 | eldifad 3959 |
. . . . . . . 8
β’ (π β π β π) |
25 | 24 | snssd 4811 |
. . . . . . 7
β’ (π β {π} β π) |
26 | 1, 3, 2, 4, 23, 12, 25 | dochocsp 40238 |
. . . . . 6
β’ (π β ( β₯
β((LSpanβπ)β{π})) = ( β₯ β{π})) |
27 | 26 | fveq2d 6892 |
. . . . 5
β’ (π β ( β₯ β( β₯
β((LSpanβπ)β{π}))) = ( β₯ β( β₯
β{π}))) |
28 | | eqid 2732 |
. . . . . . . 8
β’
((DIsoHβπΎ)βπ) = ((DIsoHβπΎ)βπ) |
29 | 1, 3, 4, 23, 28 | dihlsprn 40190 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((LSpanβπ)β{π}) β ran ((DIsoHβπΎ)βπ)) |
30 | 12, 24, 29 | syl2anc 584 |
. . . . . 6
β’ (π β ((LSpanβπ)β{π}) β ran ((DIsoHβπΎ)βπ)) |
31 | 1, 28, 2 | dochoc 40226 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((LSpanβπ)β{π}) β ran ((DIsoHβπΎ)βπ)) β ( β₯ β( β₯
β((LSpanβπ)β{π}))) = ((LSpanβπ)β{π})) |
32 | 12, 30, 31 | syl2anc 584 |
. . . . 5
β’ (π β ( β₯ β( β₯
β((LSpanβπ)β{π}))) = ((LSpanβπ)β{π})) |
33 | 22, 27, 32 | 3eqtr2d 2778 |
. . . 4
β’ (π β ( β₯ β(πΏβπΊ)) = ((LSpanβπ)β{π})) |
34 | 15, 33 | eleqtrd 2835 |
. . 3
β’ (π β π β ((LSpanβπ)β{π})) |
35 | 1, 3, 12 | dvhlmod 39969 |
. . . 4
β’ (π β π β LMod) |
36 | 9, 10, 4, 7, 23 | lspsnel 20606 |
. . . 4
β’ ((π β LMod β§ π β π) β (π β ((LSpanβπ)β{π}) β βπ β π
π = (π Β· π))) |
37 | 35, 24, 36 | syl2anc 584 |
. . 3
β’ (π β (π β ((LSpanβπ)β{π}) β βπ β π
π = (π Β· π))) |
38 | 34, 37 | mpbid 231 |
. 2
β’ (π β βπ β π
π = (π Β· π)) |
39 | | simp3 1138 |
. . . 4
β’ ((π β§ π β π
β§ π = (π Β· π)) β π = (π Β· π)) |
40 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = (π Β· π) β (πΊβπ) = (πΊβ(π Β· π))) |
41 | 40 | 3ad2ant3 1135 |
. . . . . . . . 9
β’ ((π β§ π β π
β§ π = (π Β· π)) β (πΊβπ) = (πΊβ(π Β· π))) |
42 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(1rβπ) = (1rβπ) |
43 | 1, 2, 3, 4, 6, 7, 5, 9, 10, 42, 12, 19, 18 | dochfl1 40335 |
. . . . . . . . . . 11
β’ (π β (π½βπ) = (1rβπ)) |
44 | 16 | fveq1d 6890 |
. . . . . . . . . . 11
β’ (π β (πΊβπ) = (π½βπ)) |
45 | 1, 2, 3, 4, 6, 7, 5, 9, 10, 42, 12, 13, 11 | dochfl1 40335 |
. . . . . . . . . . 11
β’ (π β (πΊβπ) = (1rβπ)) |
46 | 43, 44, 45 | 3eqtr4rd 2783 |
. . . . . . . . . 10
β’ (π β (πΊβπ) = (πΊβπ)) |
47 | 46 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π β§ π β π
β§ π = (π Β· π)) β (πΊβπ) = (πΊβπ)) |
48 | 35 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β§ π β π
β§ π = (π Β· π)) β π β LMod) |
49 | | lcfl7lem.f |
. . . . . . . . . . . 12
β’ πΉ = (LFnlβπ) |
50 | 1, 2, 3, 4, 5, 6, 7, 49, 9, 10, 11, 12, 13 | dochflcl 40334 |
. . . . . . . . . . 11
β’ (π β πΊ β πΉ) |
51 | 50 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β§ π β π
β§ π = (π Β· π)) β πΊ β πΉ) |
52 | | simp2 1137 |
. . . . . . . . . 10
β’ ((π β§ π β π
β§ π = (π Β· π)) β π β π
) |
53 | 24 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β§ π β π
β§ π = (π Β· π)) β π β π) |
54 | | eqid 2732 |
. . . . . . . . . . 11
β’
(.rβπ) = (.rβπ) |
55 | 9, 10, 54, 4, 7, 49 | lflmul 37926 |
. . . . . . . . . 10
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π
β§ π β π)) β (πΊβ(π Β· π)) = (π (.rβπ)(πΊβπ))) |
56 | 48, 51, 52, 53, 55 | syl112anc 1374 |
. . . . . . . . 9
β’ ((π β§ π β π
β§ π = (π Β· π)) β (πΊβ(π Β· π)) = (π (.rβπ)(πΊβπ))) |
57 | 41, 47, 56 | 3eqtr3d 2780 |
. . . . . . . 8
β’ ((π β§ π β π
β§ π = (π Β· π)) β (πΊβπ) = (π (.rβπ)(πΊβπ))) |
58 | 57 | oveq1d 7420 |
. . . . . . 7
β’ ((π β§ π β π
β§ π = (π Β· π)) β ((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ))) = ((π (.rβπ)(πΊβπ))(.rβπ)((invrβπ)β(πΊβπ)))) |
59 | 9 | lmodring 20471 |
. . . . . . . . . 10
β’ (π β LMod β π β Ring) |
60 | 35, 59 | syl 17 |
. . . . . . . . 9
β’ (π β π β Ring) |
61 | 60 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β§ π β π
β§ π = (π Β· π)) β π β Ring) |
62 | 9, 10, 4, 49 | lflcl 37922 |
. . . . . . . . . 10
β’ ((π β LMod β§ πΊ β πΉ β§ π β π) β (πΊβπ) β π
) |
63 | 35, 50, 24, 62 | syl3anc 1371 |
. . . . . . . . 9
β’ (π β (πΊβπ) β π
) |
64 | 63 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β§ π β π
β§ π = (π Β· π)) β (πΊβπ) β π
) |
65 | 1, 3, 12 | dvhlvec 39968 |
. . . . . . . . . . 11
β’ (π β π β LVec) |
66 | 9 | lvecdrng 20708 |
. . . . . . . . . . 11
β’ (π β LVec β π β
DivRing) |
67 | 65, 66 | syl 17 |
. . . . . . . . . 10
β’ (π β π β DivRing) |
68 | 44, 43 | eqtrd 2772 |
. . . . . . . . . . 11
β’ (π β (πΊβπ) = (1rβπ)) |
69 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(0gβπ) = (0gβπ) |
70 | 69, 42 | drngunz 20326 |
. . . . . . . . . . . 12
β’ (π β DivRing β
(1rβπ)
β (0gβπ)) |
71 | 67, 70 | syl 17 |
. . . . . . . . . . 11
β’ (π β (1rβπ) β
(0gβπ)) |
72 | 68, 71 | eqnetrd 3008 |
. . . . . . . . . 10
β’ (π β (πΊβπ) β (0gβπ)) |
73 | | eqid 2732 |
. . . . . . . . . . 11
β’
(invrβπ) = (invrβπ) |
74 | 10, 69, 73 | drnginvrcl 20329 |
. . . . . . . . . 10
β’ ((π β DivRing β§ (πΊβπ) β π
β§ (πΊβπ) β (0gβπ)) β
((invrβπ)β(πΊβπ)) β π
) |
75 | 67, 63, 72, 74 | syl3anc 1371 |
. . . . . . . . 9
β’ (π β
((invrβπ)β(πΊβπ)) β π
) |
76 | 75 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β§ π β π
β§ π = (π Β· π)) β ((invrβπ)β(πΊβπ)) β π
) |
77 | 10, 54 | ringass 20069 |
. . . . . . . 8
β’ ((π β Ring β§ (π β π
β§ (πΊβπ) β π
β§ ((invrβπ)β(πΊβπ)) β π
)) β ((π (.rβπ)(πΊβπ))(.rβπ)((invrβπ)β(πΊβπ))) = (π (.rβπ)((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ))))) |
78 | 61, 52, 64, 76, 77 | syl13anc 1372 |
. . . . . . 7
β’ ((π β§ π β π
β§ π = (π Β· π)) β ((π (.rβπ)(πΊβπ))(.rβπ)((invrβπ)β(πΊβπ))) = (π (.rβπ)((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ))))) |
79 | 10, 69, 54, 42, 73 | drnginvrr 20333 |
. . . . . . . . . 10
β’ ((π β DivRing β§ (πΊβπ) β π
β§ (πΊβπ) β (0gβπ)) β ((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ))) = (1rβπ)) |
80 | 67, 63, 72, 79 | syl3anc 1371 |
. . . . . . . . 9
β’ (π β ((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ))) = (1rβπ)) |
81 | 80 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β§ π β π
β§ π = (π Β· π)) β ((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ))) = (1rβπ)) |
82 | 81 | oveq2d 7421 |
. . . . . . 7
β’ ((π β§ π β π
β§ π = (π Β· π)) β (π (.rβπ)((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ)))) = (π (.rβπ)(1rβπ))) |
83 | 58, 78, 82 | 3eqtrrd 2777 |
. . . . . 6
β’ ((π β§ π β π
β§ π = (π Β· π)) β (π (.rβπ)(1rβπ)) = ((πΊβπ)(.rβπ)((invrβπ)β(πΊβπ)))) |
84 | 10, 54, 42 | ringridm 20080 |
. . . . . . 7
β’ ((π β Ring β§ π β π
) β (π (.rβπ)(1rβπ)) = π ) |
85 | 61, 52, 84 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π β π
β§ π = (π Β· π)) β (π (.rβπ)(1rβπ)) = π ) |
86 | 83, 85, 81 | 3eqtr3d 2780 |
. . . . 5
β’ ((π β§ π β π
β§ π = (π Β· π)) β π = (1rβπ)) |
87 | | oveq1 7412 |
. . . . . 6
β’ (π = (1rβπ) β (π Β· π) = ((1rβπ) Β· π)) |
88 | 4, 9, 7, 42 | lmodvs1 20492 |
. . . . . . . 8
β’ ((π β LMod β§ π β π) β ((1rβπ) Β· π) = π) |
89 | 35, 24, 88 | syl2anc 584 |
. . . . . . 7
β’ (π β
((1rβπ)
Β·
π) = π) |
90 | 89 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β§ π β π
β§ π = (π Β· π)) β ((1rβπ) Β· π) = π) |
91 | 87, 90 | sylan9eqr 2794 |
. . . . 5
β’ (((π β§ π β π
β§ π = (π Β· π)) β§ π = (1rβπ)) β (π Β· π) = π) |
92 | 86, 91 | mpdan 685 |
. . . 4
β’ ((π β§ π β π
β§ π = (π Β· π)) β (π Β· π) = π) |
93 | 39, 92 | eqtrd 2772 |
. . 3
β’ ((π β§ π β π
β§ π = (π Β· π)) β π = π) |
94 | 93 | rexlimdv3a 3159 |
. 2
β’ (π β (βπ β π
π = (π Β· π) β π = π)) |
95 | 38, 94 | mpd 15 |
1
β’ (π β π = π) |