| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lclkrlem2a.h |
. . . 4
β’ π» = (LHypβπΎ) |
| 2 | | eqid 2726 |
. . . 4
β’
((DIsoHβπΎ)βπ) = ((DIsoHβπΎ)βπ) |
| 3 | | lclkrlem2a.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
| 4 | | lclkrlem2a.v |
. . . 4
β’ π = (Baseβπ) |
| 5 | | lclkrlem2a.o |
. . . 4
β’ β₯ =
((ocHβπΎ)βπ) |
| 6 | | eqid 2726 |
. . . 4
β’
((joinHβπΎ)βπ) = ((joinHβπΎ)βπ) |
| 7 | | lclkrlem2a.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
| 8 | | lclkrlem2a.p |
. . . . 5
β’ β =
(LSSumβπ) |
| 9 | | lclkrlem2a.a |
. . . . 5
β’ π΄ = (LSAtomsβπ) |
| 10 | | lclkrlem2a.x |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
| 11 | 10 | eldifad 3955 |
. . . . . 6
β’ (π β π β π) |
| 12 | | lclkrlem2a.n |
. . . . . . 7
β’ π = (LSpanβπ) |
| 13 | 1, 3, 4, 12, 2 | dihlsprn 40715 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran ((DIsoHβπΎ)βπ)) |
| 14 | 7, 11, 13 | syl2anc 583 |
. . . . 5
β’ (π β (πβ{π}) β ran ((DIsoHβπΎ)βπ)) |
| 15 | | lclkrlem2a.z |
. . . . . 6
β’ 0 =
(0gβπ) |
| 16 | 1, 3, 7 | dvhlmod 40494 |
. . . . . 6
β’ (π β π β LMod) |
| 17 | | lclkrlem2a.y |
. . . . . 6
β’ (π β π β (π β { 0 })) |
| 18 | 4, 12, 15, 9, 16, 17 | lsatlspsn 38376 |
. . . . 5
β’ (π β (πβ{π}) β π΄) |
| 19 | 1, 2, 3, 8, 9, 7, 14, 18 | dihsmatrn 40820 |
. . . 4
β’ (π β ((πβ{π}) β (πβ{π})) β ran ((DIsoHβπΎ)βπ)) |
| 20 | | lclkrlem2a.b |
. . . . . . 7
β’ (π β π΅ β (π β { 0 })) |
| 21 | 20 | eldifad 3955 |
. . . . . 6
β’ (π β π΅ β π) |
| 22 | 21 | snssd 4807 |
. . . . 5
β’ (π β {π΅} β π) |
| 23 | 1, 2, 3, 4, 5 | dochcl 40737 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ {π΅} β π) β ( β₯ β{π΅}) β ran
((DIsoHβπΎ)βπ)) |
| 24 | 7, 22, 23 | syl2anc 583 |
. . . 4
β’ (π β ( β₯ β{π΅}) β ran
((DIsoHβπΎ)βπ)) |
| 25 | 1, 2, 3, 4, 5, 6, 7, 19, 24 | dochdmm1 40794 |
. . 3
β’ (π β ( β₯ β(((πβ{π}) β (πβ{π})) β© ( β₯ β{π΅}))) = (( β₯ β((πβ{π}) β (πβ{π})))((joinHβπΎ)βπ)( β₯ β( β₯
β{π΅})))) |
| 26 | 17 | eldifad 3955 |
. . . . . . . 8
β’ (π β π β π) |
| 27 | 4, 12, 8, 16, 11, 26 | lsmpr 20937 |
. . . . . . 7
β’ (π β (πβ{π, π}) = ((πβ{π}) β (πβ{π}))) |
| 28 | | df-pr 4626 |
. . . . . . . 8
β’ {π, π} = ({π} βͺ {π}) |
| 29 | 28 | fveq2i 6888 |
. . . . . . 7
β’ (πβ{π, π}) = (πβ({π} βͺ {π})) |
| 30 | 27, 29 | eqtr3di 2781 |
. . . . . 6
β’ (π β ((πβ{π}) β (πβ{π})) = (πβ({π} βͺ {π}))) |
| 31 | 30 | fveq2d 6889 |
. . . . 5
β’ (π β ( β₯ β((πβ{π}) β (πβ{π}))) = ( β₯ β(πβ({π} βͺ {π})))) |
| 32 | 11 | snssd 4807 |
. . . . . . 7
β’ (π β {π} β π) |
| 33 | 26 | snssd 4807 |
. . . . . . 7
β’ (π β {π} β π) |
| 34 | 32, 33 | unssd 4181 |
. . . . . 6
β’ (π β ({π} βͺ {π}) β π) |
| 35 | 1, 3, 5, 4, 12, 7,
34 | dochocsp 40763 |
. . . . 5
β’ (π β ( β₯ β(πβ({π} βͺ {π}))) = ( β₯ β({π} βͺ {π}))) |
| 36 | 1, 3, 4, 5 | dochdmj1 40774 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ {π} β π β§ {π} β π) β ( β₯ β({π} βͺ {π})) = (( β₯ β{π}) β© ( β₯ β{π}))) |
| 37 | 7, 32, 33, 36 | syl3anc 1368 |
. . . . 5
β’ (π β ( β₯ β({π} βͺ {π})) = (( β₯ β{π}) β© ( β₯ β{π}))) |
| 38 | 31, 35, 37 | 3eqtrd 2770 |
. . . 4
β’ (π β ( β₯ β((πβ{π}) β (πβ{π}))) = (( β₯ β{π}) β© ( β₯ β{π}))) |
| 39 | 1, 3, 5, 4, 12, 7,
21 | dochocsn 40765 |
. . . 4
β’ (π β ( β₯ β( β₯
β{π΅})) = (πβ{π΅})) |
| 40 | 38, 39 | oveq12d 7423 |
. . 3
β’ (π β (( β₯ β((πβ{π}) β (πβ{π})))((joinHβπΎ)βπ)( β₯ β( β₯
β{π΅}))) = ((( β₯
β{π}) β© ( β₯
β{π}))((joinHβπΎ)βπ)(πβ{π΅}))) |
| 41 | 1, 2, 3, 4, 5 | dochcl 40737 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ {π} β π) β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
| 42 | 7, 32, 41 | syl2anc 583 |
. . . . 5
β’ (π β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
| 43 | 1, 2, 3, 4, 5 | dochcl 40737 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ {π} β π) β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
| 44 | 7, 33, 43 | syl2anc 583 |
. . . . 5
β’ (π β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
| 45 | 1, 2 | dihmeetcl 40729 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (( β₯ β{π}) β ran
((DIsoHβπΎ)βπ) β§ ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ))) β (( β₯ β{π}) β© ( β₯ β{π})) β ran
((DIsoHβπΎ)βπ)) |
| 46 | 7, 42, 44, 45 | syl12anc 834 |
. . . 4
β’ (π β (( β₯ β{π}) β© ( β₯ β{π})) β ran
((DIsoHβπΎ)βπ)) |
| 47 | 1, 3, 4, 8, 12, 2,
6, 7, 46, 21 | dihjat1 40813 |
. . 3
β’ (π β ((( β₯ β{π}) β© ( β₯ β{π}))((joinHβπΎ)βπ)(πβ{π΅})) = ((( β₯ β{π}) β© ( β₯ β{π})) β (πβ{π΅}))) |
| 48 | 25, 40, 47 | 3eqtrrd 2771 |
. 2
β’ (π β ((( β₯ β{π}) β© ( β₯ β{π})) β (πβ{π΅})) = ( β₯ β(((πβ{π}) β (πβ{π})) β© ( β₯ β{π΅})))) |
| 49 | | lclkrlem2c.j |
. . 3
β’ π½ = (LSHypβπ) |
| 50 | | lclkrlem2a.e |
. . . 4
β’ (π β ( β₯ β{π}) β ( β₯ β{π})) |
| 51 | | lclkrlem2b.da |
. . . 4
β’ (π β (Β¬ π β ( β₯ β{π΅}) β¨ Β¬ π β ( β₯ β{π΅}))) |
| 52 | 1, 5, 3, 4, 15, 8,
12, 9, 7, 20, 10, 17, 50, 51 | lclkrlem2b 40892 |
. . 3
β’ (π β (((πβ{π}) β (πβ{π})) β© ( β₯ β{π΅})) β π΄) |
| 53 | 1, 3, 5, 9, 49, 7,
52 | dochsatshp 40835 |
. 2
β’ (π β ( β₯ β(((πβ{π}) β (πβ{π})) β© ( β₯ β{π΅}))) β π½) |
| 54 | 48, 53 | eqeltrd 2827 |
1
β’ (π β ((( β₯ β{π}) β© ( β₯ β{π})) β (πβ{π΅})) β π½) |
