Step | Hyp | Ref
| Expression |
1 | | df-pr 4627 |
. . . 4
β’ {π, π} = ({π} βͺ {π}) |
2 | 1 | fveq2i 6894 |
. . 3
β’ (πβ{π, π}) = (πβ({π} βͺ {π})) |
3 | | eqid 2727 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
4 | | dihprrnlem1.l |
. . . . 5
β’ β€ =
(leβπΎ) |
5 | | dihprrn.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | | eqid 2727 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
7 | | eqid 2727 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
8 | | dihprrn.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
9 | | eqid 2727 |
. . . . 5
β’
(LSSumβπ) =
(LSSumβπ) |
10 | | dihprrn.i |
. . . . 5
β’ πΌ = ((DIsoHβπΎ)βπ) |
11 | | dihprrn.k |
. . . . 5
β’ (π β (πΎ β HL β§ π β π»)) |
12 | | dihprrn.x |
. . . . . . . 8
β’ (π β π β π) |
13 | | dihprrn.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
14 | | dihprrn.n |
. . . . . . . . 9
β’ π = (LSpanβπ) |
15 | 5, 8, 13, 14, 10 | dihlsprn 40728 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran πΌ) |
16 | 11, 12, 15 | syl2anc 583 |
. . . . . . 7
β’ (π β (πβ{π}) β ran πΌ) |
17 | 3, 5, 10 | dihcnvcl 40668 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πβ{π}) β ran πΌ) β (β‘πΌβ(πβ{π})) β (BaseβπΎ)) |
18 | 11, 16, 17 | syl2anc 583 |
. . . . . 6
β’ (π β (β‘πΌβ(πβ{π})) β (BaseβπΎ)) |
19 | | dihprrnlem1.x |
. . . . . 6
β’ (π β (β‘πΌβ(πβ{π})) β€ π) |
20 | 18, 19 | jca 511 |
. . . . 5
β’ (π β ((β‘πΌβ(πβ{π})) β (BaseβπΎ) β§ (β‘πΌβ(πβ{π})) β€ π)) |
21 | | dihprrn.y |
. . . . . . 7
β’ (π β π β π) |
22 | | dihprrnlem1.nz |
. . . . . . 7
β’ (π β π β 0 ) |
23 | | dihprrnlem1.o |
. . . . . . . 8
β’ 0 =
(0gβπ) |
24 | 7, 5, 8, 13, 23, 14, 10 | dihlspsnat 40730 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (β‘πΌβ(πβ{π})) β (AtomsβπΎ)) |
25 | 11, 21, 22, 24 | syl3anc 1369 |
. . . . . 6
β’ (π β (β‘πΌβ(πβ{π})) β (AtomsβπΎ)) |
26 | | dihprrnlem1.y |
. . . . . 6
β’ (π β Β¬ (β‘πΌβ(πβ{π})) β€ π) |
27 | 25, 26 | jca 511 |
. . . . 5
β’ (π β ((β‘πΌβ(πβ{π})) β (AtomsβπΎ) β§ Β¬ (β‘πΌβ(πβ{π})) β€ π)) |
28 | 3, 4, 5, 6, 7, 8, 9, 10, 11, 20, 27 | dihjatc 40814 |
. . . 4
β’ (π β (πΌβ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π})))) = ((πΌβ(β‘πΌβ(πβ{π})))(LSSumβπ)(πΌβ(β‘πΌβ(πβ{π}))))) |
29 | 5, 10 | dihcnvid2 40670 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πβ{π}) β ran πΌ) β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
30 | 11, 16, 29 | syl2anc 583 |
. . . . 5
β’ (π β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
31 | 5, 8, 13, 14, 10 | dihlsprn 40728 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran πΌ) |
32 | 11, 21, 31 | syl2anc 583 |
. . . . . 6
β’ (π β (πβ{π}) β ran πΌ) |
33 | 5, 10 | dihcnvid2 40670 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πβ{π}) β ran πΌ) β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
34 | 11, 32, 33 | syl2anc 583 |
. . . . 5
β’ (π β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
35 | 30, 34 | oveq12d 7432 |
. . . 4
β’ (π β ((πΌβ(β‘πΌβ(πβ{π})))(LSSumβπ)(πΌβ(β‘πΌβ(πβ{π})))) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
36 | 5, 8, 11 | dvhlmod 40507 |
. . . . 5
β’ (π β π β LMod) |
37 | 12 | snssd 4808 |
. . . . 5
β’ (π β {π} β π) |
38 | 21 | snssd 4808 |
. . . . 5
β’ (π β {π} β π) |
39 | 13, 14, 9 | lsmsp2 20954 |
. . . . 5
β’ ((π β LMod β§ {π} β π β§ {π} β π) β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ({π} βͺ {π}))) |
40 | 36, 37, 38, 39 | syl3anc 1369 |
. . . 4
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ({π} βͺ {π}))) |
41 | 28, 35, 40 | 3eqtrrd 2772 |
. . 3
β’ (π β (πβ({π} βͺ {π})) = (πΌβ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π}))))) |
42 | 2, 41 | eqtrid 2779 |
. 2
β’ (π β (πβ{π, π}) = (πΌβ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π}))))) |
43 | 11 | simpld 494 |
. . . . 5
β’ (π β πΎ β HL) |
44 | 43 | hllatd 38760 |
. . . 4
β’ (π β πΎ β Lat) |
45 | 3, 5, 10 | dihcnvcl 40668 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβ{π}) β ran πΌ) β (β‘πΌβ(πβ{π})) β (BaseβπΎ)) |
46 | 11, 32, 45 | syl2anc 583 |
. . . 4
β’ (π β (β‘πΌβ(πβ{π})) β (BaseβπΎ)) |
47 | 3, 6 | latjcl 18416 |
. . . 4
β’ ((πΎ β Lat β§ (β‘πΌβ(πβ{π})) β (BaseβπΎ) β§ (β‘πΌβ(πβ{π})) β (BaseβπΎ)) β ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π}))) β (BaseβπΎ)) |
48 | 44, 18, 46, 47 | syl3anc 1369 |
. . 3
β’ (π β ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π}))) β (BaseβπΎ)) |
49 | 3, 5, 10 | dihcl 40667 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π}))) β (BaseβπΎ)) β (πΌβ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π})))) β ran πΌ) |
50 | 11, 48, 49 | syl2anc 583 |
. 2
β’ (π β (πΌβ((β‘πΌβ(πβ{π}))(joinβπΎ)(β‘πΌβ(πβ{π})))) β ran πΌ) |
51 | 42, 50 | eqeltrd 2828 |
1
β’ (π β (πβ{π, π}) β ran πΌ) |