Step | Hyp | Ref
| Expression |
1 | | mapdlsm.h |
. . . . . . . . . . 11
β’ π» = (LHypβπΎ) |
2 | | mapdlsm.c |
. . . . . . . . . . 11
β’ πΆ = ((LCDualβπΎ)βπ) |
3 | | mapdlsm.k |
. . . . . . . . . . 11
β’ (π β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | lcdlmod 40105 |
. . . . . . . . . 10
β’ (π β πΆ β LMod) |
5 | | eqid 2733 |
. . . . . . . . . . 11
β’
(LSubSpβπΆ) =
(LSubSpβπΆ) |
6 | 5 | lsssssubg 20463 |
. . . . . . . . . 10
β’ (πΆ β LMod β
(LSubSpβπΆ) β
(SubGrpβπΆ)) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
β’ (π β (LSubSpβπΆ) β (SubGrpβπΆ)) |
8 | | mapdlsm.m |
. . . . . . . . . 10
β’ π = ((mapdβπΎ)βπ) |
9 | | mapdlsm.u |
. . . . . . . . . 10
β’ π = ((DVecHβπΎ)βπ) |
10 | | mapdlsm.s |
. . . . . . . . . 10
β’ π = (LSubSpβπ) |
11 | | mapdlsm.x |
. . . . . . . . . 10
β’ (π β π β π) |
12 | 1, 8, 9, 10, 2, 5,
3, 11 | mapdcl2 40169 |
. . . . . . . . 9
β’ (π β (πβπ) β (LSubSpβπΆ)) |
13 | 7, 12 | sseldd 3949 |
. . . . . . . 8
β’ (π β (πβπ) β (SubGrpβπΆ)) |
14 | | mapdlsm.y |
. . . . . . . . . 10
β’ (π β π β π) |
15 | 1, 8, 9, 10, 2, 5,
3, 14 | mapdcl2 40169 |
. . . . . . . . 9
β’ (π β (πβπ) β (LSubSpβπΆ)) |
16 | 7, 15 | sseldd 3949 |
. . . . . . . 8
β’ (π β (πβπ) β (SubGrpβπΆ)) |
17 | | mapdlsm.q |
. . . . . . . . 9
β’ β =
(LSSumβπΆ) |
18 | 17 | lsmub1 19447 |
. . . . . . . 8
β’ (((πβπ) β (SubGrpβπΆ) β§ (πβπ) β (SubGrpβπΆ)) β (πβπ) β ((πβπ) β (πβπ))) |
19 | 13, 16, 18 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβπ) β ((πβπ) β (πβπ))) |
20 | 1, 8, 9, 10, 3, 11 | mapdcl 40166 |
. . . . . . . . 9
β’ (π β (πβπ) β ran π) |
21 | 1, 8, 9, 10, 3, 14 | mapdcl 40166 |
. . . . . . . . 9
β’ (π β (πβπ) β ran π) |
22 | 1, 8, 9, 2, 17, 3,
20, 21 | mapdlsmcl 40176 |
. . . . . . . 8
β’ (π β ((πβπ) β (πβπ)) β ran π) |
23 | 1, 8, 3, 22 | mapdcnvid2 40170 |
. . . . . . 7
β’ (π β (πβ(β‘πβ((πβπ) β (πβπ)))) = ((πβπ) β (πβπ))) |
24 | 19, 23 | sseqtrrd 3989 |
. . . . . 6
β’ (π β (πβπ) β (πβ(β‘πβ((πβπ) β (πβπ))))) |
25 | 1, 8, 9, 10, 3, 22 | mapdcnvcl 40165 |
. . . . . . 7
β’ (π β (β‘πβ((πβπ) β (πβπ))) β π) |
26 | 1, 9, 10, 8, 3, 11, 25 | mapdord 40151 |
. . . . . 6
β’ (π β ((πβπ) β (πβ(β‘πβ((πβπ) β (πβπ)))) β π β (β‘πβ((πβπ) β (πβπ))))) |
27 | 24, 26 | mpbid 231 |
. . . . 5
β’ (π β π β (β‘πβ((πβπ) β (πβπ)))) |
28 | 17 | lsmub2 19448 |
. . . . . . . 8
β’ (((πβπ) β (SubGrpβπΆ) β§ (πβπ) β (SubGrpβπΆ)) β (πβπ) β ((πβπ) β (πβπ))) |
29 | 13, 16, 28 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβπ) β ((πβπ) β (πβπ))) |
30 | 29, 23 | sseqtrrd 3989 |
. . . . . 6
β’ (π β (πβπ) β (πβ(β‘πβ((πβπ) β (πβπ))))) |
31 | 1, 9, 10, 8, 3, 14, 25 | mapdord 40151 |
. . . . . 6
β’ (π β ((πβπ) β (πβ(β‘πβ((πβπ) β (πβπ)))) β π β (β‘πβ((πβπ) β (πβπ))))) |
32 | 30, 31 | mpbid 231 |
. . . . 5
β’ (π β π β (β‘πβ((πβπ) β (πβπ)))) |
33 | 1, 9, 3 | dvhlmod 39623 |
. . . . . . . 8
β’ (π β π β LMod) |
34 | 10 | lsssssubg 20463 |
. . . . . . . 8
β’ (π β LMod β π β (SubGrpβπ)) |
35 | 33, 34 | syl 17 |
. . . . . . 7
β’ (π β π β (SubGrpβπ)) |
36 | 35, 11 | sseldd 3949 |
. . . . . 6
β’ (π β π β (SubGrpβπ)) |
37 | 35, 14 | sseldd 3949 |
. . . . . 6
β’ (π β π β (SubGrpβπ)) |
38 | 35, 25 | sseldd 3949 |
. . . . . 6
β’ (π β (β‘πβ((πβπ) β (πβπ))) β (SubGrpβπ)) |
39 | | mapdlsm.p |
. . . . . . 7
β’ β =
(LSSumβπ) |
40 | 39 | lsmlub 19454 |
. . . . . 6
β’ ((π β (SubGrpβπ) β§ π β (SubGrpβπ) β§ (β‘πβ((πβπ) β (πβπ))) β (SubGrpβπ)) β ((π β (β‘πβ((πβπ) β (πβπ))) β§ π β (β‘πβ((πβπ) β (πβπ)))) β (π β π) β (β‘πβ((πβπ) β (πβπ))))) |
41 | 36, 37, 38, 40 | syl3anc 1372 |
. . . . 5
β’ (π β ((π β (β‘πβ((πβπ) β (πβπ))) β§ π β (β‘πβ((πβπ) β (πβπ)))) β (π β π) β (β‘πβ((πβπ) β (πβπ))))) |
42 | 27, 32, 41 | mpbi2and 711 |
. . . 4
β’ (π β (π β π) β (β‘πβ((πβπ) β (πβπ)))) |
43 | 10, 39 | lsmcl 20588 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
44 | 33, 11, 14, 43 | syl3anc 1372 |
. . . . 5
β’ (π β (π β π) β π) |
45 | 1, 9, 10, 8, 3, 44, 25 | mapdord 40151 |
. . . 4
β’ (π β ((πβ(π β π)) β (πβ(β‘πβ((πβπ) β (πβπ)))) β (π β π) β (β‘πβ((πβπ) β (πβπ))))) |
46 | 42, 45 | mpbird 257 |
. . 3
β’ (π β (πβ(π β π)) β (πβ(β‘πβ((πβπ) β (πβπ))))) |
47 | 46, 23 | sseqtrd 3988 |
. 2
β’ (π β (πβ(π β π)) β ((πβπ) β (πβπ))) |
48 | 39 | lsmub1 19447 |
. . . . 5
β’ ((π β (SubGrpβπ) β§ π β (SubGrpβπ)) β π β (π β π)) |
49 | 36, 37, 48 | syl2anc 585 |
. . . 4
β’ (π β π β (π β π)) |
50 | 1, 9, 10, 8, 3, 11, 44 | mapdord 40151 |
. . . 4
β’ (π β ((πβπ) β (πβ(π β π)) β π β (π β π))) |
51 | 49, 50 | mpbird 257 |
. . 3
β’ (π β (πβπ) β (πβ(π β π))) |
52 | 39 | lsmub2 19448 |
. . . . 5
β’ ((π β (SubGrpβπ) β§ π β (SubGrpβπ)) β π β (π β π)) |
53 | 36, 37, 52 | syl2anc 585 |
. . . 4
β’ (π β π β (π β π)) |
54 | 1, 9, 10, 8, 3, 14, 44 | mapdord 40151 |
. . . 4
β’ (π β ((πβπ) β (πβ(π β π)) β π β (π β π))) |
55 | 53, 54 | mpbird 257 |
. . 3
β’ (π β (πβπ) β (πβ(π β π))) |
56 | 1, 8, 9, 10, 2, 5,
3, 44 | mapdcl2 40169 |
. . . . 5
β’ (π β (πβ(π β π)) β (LSubSpβπΆ)) |
57 | 7, 56 | sseldd 3949 |
. . . 4
β’ (π β (πβ(π β π)) β (SubGrpβπΆ)) |
58 | 17 | lsmlub 19454 |
. . . 4
β’ (((πβπ) β (SubGrpβπΆ) β§ (πβπ) β (SubGrpβπΆ) β§ (πβ(π β π)) β (SubGrpβπΆ)) β (((πβπ) β (πβ(π β π)) β§ (πβπ) β (πβ(π β π))) β ((πβπ) β (πβπ)) β (πβ(π β π)))) |
59 | 13, 16, 57, 58 | syl3anc 1372 |
. . 3
β’ (π β (((πβπ) β (πβ(π β π)) β§ (πβπ) β (πβ(π β π))) β ((πβπ) β (πβπ)) β (πβ(π β π)))) |
60 | 51, 55, 59 | mpbi2and 711 |
. 2
β’ (π β ((πβπ) β (πβπ)) β (πβ(π β π))) |
61 | 47, 60 | eqssd 3965 |
1
β’ (π β (πβ(π β π)) = ((πβπ) β (πβπ))) |