Step | Hyp | Ref
| Expression |
1 | | lveclmod 20716 |
. . . . 5
β’ (π β LVec β π β LMod) |
2 | 1 | 3ad2ant1 1133 |
. . . 4
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β π β LMod) |
3 | | simp2r 1200 |
. . . . 5
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β πΊ β πΉ) |
4 | | lkrlsp.f |
. . . . . 6
β’ πΉ = (LFnlβπ) |
5 | | lkrlsp.k |
. . . . . 6
β’ πΎ = (LKerβπ) |
6 | | eqid 2732 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
7 | 4, 5, 6 | lkrlss 37960 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ) β (πΎβπΊ) β (LSubSpβπ)) |
8 | 2, 3, 7 | syl2anc 584 |
. . . 4
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β (πΎβπΊ) β (LSubSpβπ)) |
9 | | simp2l 1199 |
. . . . 5
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β π β π) |
10 | | lkrlsp.v |
. . . . . 6
β’ π = (Baseβπ) |
11 | | lkrlsp.n |
. . . . . 6
β’ π = (LSpanβπ) |
12 | 10, 6, 11 | lspsncl 20587 |
. . . . 5
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
13 | 2, 9, 12 | syl2anc 584 |
. . . 4
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β (πβ{π}) β (LSubSpβπ)) |
14 | | lkrlsp.p |
. . . . 5
β’ β =
(LSSumβπ) |
15 | 6, 14 | lsmcl 20693 |
. . . 4
β’ ((π β LMod β§ (πΎβπΊ) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πΎβπΊ) β (πβ{π})) β (LSubSpβπ)) |
16 | 2, 8, 13, 15 | syl3anc 1371 |
. . 3
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β ((πΎβπΊ) β (πβ{π})) β (LSubSpβπ)) |
17 | 10, 6 | lssss 20546 |
. . 3
β’ (((πΎβπΊ) β (πβ{π})) β (LSubSpβπ) β ((πΎβπΊ) β (πβ{π})) β π) |
18 | 16, 17 | syl 17 |
. 2
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β ((πΎβπΊ) β (πβ{π})) β π) |
19 | | simpl1 1191 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π β LVec) |
20 | 19, 1 | syl 17 |
. . . 4
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π β LMod) |
21 | | simpr 485 |
. . . 4
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π’ β π) |
22 | | lkrlsp.d |
. . . . . . . 8
β’ π· = (Scalarβπ) |
23 | 22 | lmodring 20478 |
. . . . . . 7
β’ (π β LMod β π· β Ring) |
24 | 20, 23 | syl 17 |
. . . . . 6
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π· β Ring) |
25 | | simpl2r 1227 |
. . . . . . 7
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β πΊ β πΉ) |
26 | | eqid 2732 |
. . . . . . . 8
β’
(Baseβπ·) =
(Baseβπ·) |
27 | 22, 26, 10, 4 | lflcl 37929 |
. . . . . . 7
β’ ((π β LVec β§ πΊ β πΉ β§ π’ β π) β (πΊβπ’) β (Baseβπ·)) |
28 | 19, 25, 21, 27 | syl3anc 1371 |
. . . . . 6
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΊβπ’) β (Baseβπ·)) |
29 | 22 | lvecdrng 20715 |
. . . . . . . 8
β’ (π β LVec β π· β
DivRing) |
30 | 19, 29 | syl 17 |
. . . . . . 7
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π· β DivRing) |
31 | | simpl2l 1226 |
. . . . . . . 8
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π β π) |
32 | 22, 26, 10, 4 | lflcl 37929 |
. . . . . . . 8
β’ ((π β LVec β§ πΊ β πΉ β§ π β π) β (πΊβπ) β (Baseβπ·)) |
33 | 19, 25, 31, 32 | syl3anc 1371 |
. . . . . . 7
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΊβπ) β (Baseβπ·)) |
34 | | simpl3 1193 |
. . . . . . 7
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΊβπ) β 0 ) |
35 | | lkrlsp.o |
. . . . . . . 8
β’ 0 =
(0gβπ·) |
36 | | eqid 2732 |
. . . . . . . 8
β’
(invrβπ·) = (invrβπ·) |
37 | 26, 35, 36 | drnginvrcl 20378 |
. . . . . . 7
β’ ((π· β DivRing β§ (πΊβπ) β (Baseβπ·) β§ (πΊβπ) β 0 ) β
((invrβπ·)β(πΊβπ)) β (Baseβπ·)) |
38 | 30, 33, 34, 37 | syl3anc 1371 |
. . . . . 6
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((invrβπ·)β(πΊβπ)) β (Baseβπ·)) |
39 | | eqid 2732 |
. . . . . . 7
β’
(.rβπ·) = (.rβπ·) |
40 | 26, 39 | ringcl 20072 |
. . . . . 6
β’ ((π· β Ring β§ (πΊβπ’) β (Baseβπ·) β§ ((invrβπ·)β(πΊβπ)) β (Baseβπ·)) β ((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ))) β (Baseβπ·)) |
41 | 24, 28, 38, 40 | syl3anc 1371 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ))) β (Baseβπ·)) |
42 | | eqid 2732 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
43 | 10, 22, 42, 26 | lmodvscl 20488 |
. . . . 5
β’ ((π β LMod β§ ((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ))) β (Baseβπ·) β§ π β π) β (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π) β π) |
44 | 20, 41, 31, 43 | syl3anc 1371 |
. . . 4
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π) β π) |
45 | | eqid 2732 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
46 | | eqid 2732 |
. . . . 5
β’
(-gβπ) = (-gβπ) |
47 | 10, 45, 46 | lmodvnpcan 20525 |
. . . 4
β’ ((π β LMod β§ π’ β π β§ (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π) β π) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))(+gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) = π’) |
48 | 20, 21, 44, 47 | syl3anc 1371 |
. . 3
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))(+gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) = π’) |
49 | 6 | lsssssubg 20568 |
. . . . . 6
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
50 | 20, 49 | syl 17 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (LSubSpβπ) β (SubGrpβπ)) |
51 | 8 | adantr 481 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΎβπΊ) β (LSubSpβπ)) |
52 | 50, 51 | sseldd 3983 |
. . . 4
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΎβπΊ) β (SubGrpβπ)) |
53 | 13 | adantr 481 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πβ{π}) β (LSubSpβπ)) |
54 | 50, 53 | sseldd 3983 |
. . . 4
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πβ{π}) β (SubGrpβπ)) |
55 | 10, 46 | lmodvsubcl 20516 |
. . . . . 6
β’ ((π β LMod β§ π’ β π β§ (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π) β π) β (π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β π) |
56 | 20, 21, 44, 55 | syl3anc 1371 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β π) |
57 | | eqid 2732 |
. . . . . . . 8
β’
(-gβπ·) = (-gβπ·) |
58 | 22, 57, 10, 46, 4 | lflsub 37932 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ (π’ β π β§ (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π) β π)) β (πΊβ(π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))) = ((πΊβπ’)(-gβπ·)(πΊβ(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)))) |
59 | 20, 25, 21, 44, 58 | syl112anc 1374 |
. . . . . 6
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΊβ(π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))) = ((πΊβπ’)(-gβπ·)(πΊβ(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)))) |
60 | 22, 26, 39, 10, 42, 4 | lflmul 37933 |
. . . . . . . . 9
β’ ((π β LMod β§ πΊ β πΉ β§ (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ))) β (Baseβπ·) β§ π β π)) β (πΊβ(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) = (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))(.rβπ·)(πΊβπ))) |
61 | 20, 25, 41, 31, 60 | syl112anc 1374 |
. . . . . . . 8
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΊβ(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) = (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))(.rβπ·)(πΊβπ))) |
62 | 26, 39 | ringass 20075 |
. . . . . . . . 9
β’ ((π· β Ring β§ ((πΊβπ’) β (Baseβπ·) β§ ((invrβπ·)β(πΊβπ)) β (Baseβπ·) β§ (πΊβπ) β (Baseβπ·))) β (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))(.rβπ·)(πΊβπ)) = ((πΊβπ’)(.rβπ·)(((invrβπ·)β(πΊβπ))(.rβπ·)(πΊβπ)))) |
63 | 24, 28, 38, 33, 62 | syl13anc 1372 |
. . . . . . . 8
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))(.rβπ·)(πΊβπ)) = ((πΊβπ’)(.rβπ·)(((invrβπ·)β(πΊβπ))(.rβπ·)(πΊβπ)))) |
64 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(1rβπ·) = (1rβπ·) |
65 | 26, 35, 39, 64, 36 | drnginvrl 20381 |
. . . . . . . . . . 11
β’ ((π· β DivRing β§ (πΊβπ) β (Baseβπ·) β§ (πΊβπ) β 0 ) β
(((invrβπ·)β(πΊβπ))(.rβπ·)(πΊβπ)) = (1rβπ·)) |
66 | 30, 33, 34, 65 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (((invrβπ·)β(πΊβπ))(.rβπ·)(πΊβπ)) = (1rβπ·)) |
67 | 66 | oveq2d 7424 |
. . . . . . . . 9
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((πΊβπ’)(.rβπ·)(((invrβπ·)β(πΊβπ))(.rβπ·)(πΊβπ))) = ((πΊβπ’)(.rβπ·)(1rβπ·))) |
68 | 26, 39, 64 | ringridm 20086 |
. . . . . . . . . 10
β’ ((π· β Ring β§ (πΊβπ’) β (Baseβπ·)) β ((πΊβπ’)(.rβπ·)(1rβπ·)) = (πΊβπ’)) |
69 | 24, 28, 68 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((πΊβπ’)(.rβπ·)(1rβπ·)) = (πΊβπ’)) |
70 | 67, 69 | eqtrd 2772 |
. . . . . . . 8
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((πΊβπ’)(.rβπ·)(((invrβπ·)β(πΊβπ))(.rβπ·)(πΊβπ))) = (πΊβπ’)) |
71 | 61, 63, 70 | 3eqtrd 2776 |
. . . . . . 7
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΊβ(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) = (πΊβπ’)) |
72 | 71 | oveq2d 7424 |
. . . . . 6
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((πΊβπ’)(-gβπ·)(πΊβ(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))) = ((πΊβπ’)(-gβπ·)(πΊβπ’))) |
73 | 22 | lmodfgrp 20479 |
. . . . . . . 8
β’ (π β LMod β π· β Grp) |
74 | 20, 73 | syl 17 |
. . . . . . 7
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π· β Grp) |
75 | 26, 35, 57 | grpsubid 18906 |
. . . . . . 7
β’ ((π· β Grp β§ (πΊβπ’) β (Baseβπ·)) β ((πΊβπ’)(-gβπ·)(πΊβπ’)) = 0 ) |
76 | 74, 28, 75 | syl2anc 584 |
. . . . . 6
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((πΊβπ’)(-gβπ·)(πΊβπ’)) = 0 ) |
77 | 59, 72, 76 | 3eqtrd 2776 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (πΊβ(π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))) = 0 ) |
78 | 10, 22, 35, 4, 5 | ellkr 37954 |
. . . . . 6
β’ ((π β LVec β§ πΊ β πΉ) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β (πΎβπΊ) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β π β§ (πΊβ(π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))) = 0 ))) |
79 | 19, 25, 78 | syl2anc 584 |
. . . . 5
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β (πΎβπΊ) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β π β§ (πΊβ(π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))) = 0 ))) |
80 | 56, 77, 79 | mpbir2and 711 |
. . . 4
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β (πΎβπΊ)) |
81 | 10, 42, 22, 26, 11, 20, 41, 31 | lspsneli 20611 |
. . . 4
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π) β (πβ{π})) |
82 | 45, 14 | lsmelvali 19517 |
. . . 4
β’ ((((πΎβπΊ) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β§ ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β (πΎβπΊ) β§ (((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π) β (πβ{π}))) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))(+gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β ((πΎβπΊ) β (πβ{π}))) |
83 | 52, 54, 80, 81, 82 | syl22anc 837 |
. . 3
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β ((π’(-gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π))(+gβπ)(((πΊβπ’)(.rβπ·)((invrβπ·)β(πΊβπ)))( Β·π
βπ)π)) β ((πΎβπΊ) β (πβ{π}))) |
84 | 48, 83 | eqeltrrd 2834 |
. 2
β’ (((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β§ π’ β π) β π’ β ((πΎβπΊ) β (πβ{π}))) |
85 | 18, 84 | eqelssd 4003 |
1
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ (πΊβπ) β 0 ) β ((πΎβπΊ) β (πβ{π})) = π) |