Step | Hyp | Ref
| Expression |
1 | | ocvpj.k |
. . . . . 6
β’ πΎ = (projβπ) |
2 | | eqid 2737 |
. . . . . 6
β’
(ClSubSpβπ) =
(ClSubSpβπ) |
3 | 1, 2 | pjcss 21138 |
. . . . 5
β’ (π β PreHil β dom πΎ β (ClSubSpβπ)) |
4 | 3 | sselda 3949 |
. . . 4
β’ ((π β PreHil β§ π β dom πΎ) β π β (ClSubSpβπ)) |
5 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
6 | 5, 2 | cssss 21105 |
. . . 4
β’ (π β (ClSubSpβπ) β π β (Baseβπ)) |
7 | 4, 6 | syl 17 |
. . 3
β’ ((π β PreHil β§ π β dom πΎ) β π β (Baseβπ)) |
8 | | ocvpj.o |
. . . 4
β’ β₯ =
(ocvβπ) |
9 | | eqid 2737 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
10 | 5, 8, 9 | ocvlss 21092 |
. . 3
β’ ((π β PreHil β§ π β (Baseβπ)) β ( β₯ βπ) β (LSubSpβπ)) |
11 | 7, 10 | syldan 592 |
. 2
β’ ((π β PreHil β§ π β dom πΎ) β ( β₯ βπ) β (LSubSpβπ)) |
12 | | phllmod 21050 |
. . . . . 6
β’ (π β PreHil β π β LMod) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β PreHil β§ π β dom πΎ) β π β LMod) |
14 | | lmodabl 20385 |
. . . . 5
β’ (π β LMod β π β Abel) |
15 | 13, 14 | syl 17 |
. . . 4
β’ ((π β PreHil β§ π β dom πΎ) β π β Abel) |
16 | 9 | lsssssubg 20435 |
. . . . . 6
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
17 | 13, 16 | syl 17 |
. . . . 5
β’ ((π β PreHil β§ π β dom πΎ) β (LSubSpβπ) β (SubGrpβπ)) |
18 | 17, 11 | sseldd 3950 |
. . . 4
β’ ((π β PreHil β§ π β dom πΎ) β ( β₯ βπ) β (SubGrpβπ)) |
19 | 2, 9 | csslss 21111 |
. . . . . 6
β’ ((π β PreHil β§ π β (ClSubSpβπ)) β π β (LSubSpβπ)) |
20 | 4, 19 | syldan 592 |
. . . . 5
β’ ((π β PreHil β§ π β dom πΎ) β π β (LSubSpβπ)) |
21 | 17, 20 | sseldd 3950 |
. . . 4
β’ ((π β PreHil β§ π β dom πΎ) β π β (SubGrpβπ)) |
22 | | eqid 2737 |
. . . . 5
β’
(LSSumβπ) =
(LSSumβπ) |
23 | 22 | lsmcom 19643 |
. . . 4
β’ ((π β Abel β§ ( β₯
βπ) β
(SubGrpβπ) β§
π β
(SubGrpβπ)) β ((
β₯
βπ)(LSSumβπ)π) = (π(LSSumβπ)( β₯ βπ))) |
24 | 15, 18, 21, 23 | syl3anc 1372 |
. . 3
β’ ((π β PreHil β§ π β dom πΎ) β (( β₯ βπ)(LSSumβπ)π) = (π(LSSumβπ)( β₯ βπ))) |
25 | 8, 2 | cssi 21104 |
. . . . 5
β’ (π β (ClSubSpβπ) β π = ( β₯ β( β₯
βπ))) |
26 | 4, 25 | syl 17 |
. . . 4
β’ ((π β PreHil β§ π β dom πΎ) β π = ( β₯ β( β₯
βπ))) |
27 | 26 | oveq2d 7378 |
. . 3
β’ ((π β PreHil β§ π β dom πΎ) β (( β₯ βπ)(LSSumβπ)π) = (( β₯ βπ)(LSSumβπ)( β₯ β( β₯
βπ)))) |
28 | 5, 9, 8, 22, 1 | pjdm2 21133 |
. . . 4
β’ (π β PreHil β (π β dom πΎ β (π β (LSubSpβπ) β§ (π(LSSumβπ)( β₯ βπ)) = (Baseβπ)))) |
29 | 28 | simplbda 501 |
. . 3
β’ ((π β PreHil β§ π β dom πΎ) β (π(LSSumβπ)( β₯ βπ)) = (Baseβπ)) |
30 | 24, 27, 29 | 3eqtr3d 2785 |
. 2
β’ ((π β PreHil β§ π β dom πΎ) β (( β₯ βπ)(LSSumβπ)( β₯ β( β₯
βπ))) =
(Baseβπ)) |
31 | 5, 9, 8, 22, 1 | pjdm2 21133 |
. . 3
β’ (π β PreHil β (( β₯
βπ) β dom πΎ β (( β₯ βπ) β (LSubSpβπ) β§ (( β₯ βπ)(LSSumβπ)( β₯ β( β₯
βπ))) =
(Baseβπ)))) |
32 | 31 | adantr 482 |
. 2
β’ ((π β PreHil β§ π β dom πΎ) β (( β₯ βπ) β dom πΎ β (( β₯ βπ) β (LSubSpβπ) β§ (( β₯ βπ)(LSSumβπ)( β₯ β( β₯
βπ))) =
(Baseβπ)))) |
33 | 11, 30, 32 | mpbir2and 712 |
1
β’ ((π β PreHil β§ π β dom πΎ) β ( β₯ βπ) β dom πΎ) |