Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
2 | | dochnoncon.s |
. . . . . 6
β’ π = (LSubSpβπ) |
3 | 1, 2 | lssss 20552 |
. . . . 5
β’ (π β π β π β (Baseβπ)) |
4 | | dochnoncon.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
5 | | dochnoncon.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
6 | | dochnoncon.o |
. . . . . 6
β’ β₯ =
((ocHβπΎ)βπ) |
7 | 4, 5, 1, 6 | dochocss 40329 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (Baseβπ)) β π β ( β₯ β( β₯
βπ))) |
8 | 3, 7 | sylan2 593 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β ( β₯ β( β₯
βπ))) |
9 | 8 | ssrind 4235 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π β© ( β₯ βπ)) β (( β₯ β( β₯
βπ)) β© ( β₯
βπ))) |
10 | | simpl 483 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΎ β HL β§ π β π»)) |
11 | | eqid 2732 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
12 | | eqid 2732 |
. . . . . . . . . 10
β’
((DIsoHβπΎ)βπ) = ((DIsoHβπΎ)βπ) |
13 | | eqid 2732 |
. . . . . . . . . 10
β’
(LSubSpβπ) =
(LSubSpβπ) |
14 | 11, 4, 12, 5, 13 | dihf11 40230 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β ((DIsoHβπΎ)βπ):(BaseβπΎ)β1-1β(LSubSpβπ)) |
15 | 14 | adantr 481 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((DIsoHβπΎ)βπ):(BaseβπΎ)β1-1β(LSubSpβπ)) |
16 | | f1f1orn 6844 |
. . . . . . . 8
β’
(((DIsoHβπΎ)βπ):(BaseβπΎ)β1-1β(LSubSpβπ) β ((DIsoHβπΎ)βπ):(BaseβπΎ)β1-1-ontoβran
((DIsoHβπΎ)βπ)) |
17 | 15, 16 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((DIsoHβπΎ)βπ):(BaseβπΎ)β1-1-ontoβran
((DIsoHβπΎ)βπ)) |
18 | 4, 12, 5, 1, 6 | dochcl 40316 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π β (Baseβπ)) β ( β₯ βπ) β ran ((DIsoHβπΎ)βπ)) |
19 | 3, 18 | sylan2 593 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β ran ((DIsoHβπΎ)βπ)) |
20 | 4, 5, 12, 13 | dihrnlss 40240 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β ran ((DIsoHβπΎ)βπ)) β ( β₯ βπ) β (LSubSpβπ)) |
21 | 19, 20 | syldan 591 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β (LSubSpβπ)) |
22 | 1, 13 | lssss 20552 |
. . . . . . . . 9
β’ (( β₯
βπ) β
(LSubSpβπ) β (
β₯
βπ) β
(Baseβπ)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β (Baseβπ)) |
24 | 4, 12, 5, 1, 6 | dochcl 40316 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β (Baseβπ)) β ( β₯ β( β₯
βπ)) β ran
((DIsoHβπΎ)βπ)) |
25 | 23, 24 | syldan 591 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ β( β₯
βπ)) β ran
((DIsoHβπΎ)βπ)) |
26 | | f1ocnvdm 7285 |
. . . . . . 7
β’
((((DIsoHβπΎ)βπ):(BaseβπΎ)β1-1-ontoβran
((DIsoHβπΎ)βπ) β§ ( β₯ β( β₯
βπ)) β ran
((DIsoHβπΎ)βπ)) β (β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))) β
(BaseβπΎ)) |
27 | 17, 25, 26 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β (β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))) β
(BaseβπΎ)) |
28 | | hlop 38324 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OP) |
29 | 28 | ad2antrr 724 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β πΎ β OP) |
30 | | eqid 2732 |
. . . . . . . 8
β’
(ocβπΎ) =
(ocβπΎ) |
31 | 11, 30 | opoccl 38156 |
. . . . . . 7
β’ ((πΎ β OP β§ (β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))) β
(BaseβπΎ)) β
((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) β
(BaseβπΎ)) |
32 | 29, 27, 31 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) β
(BaseβπΎ)) |
33 | | eqid 2732 |
. . . . . . 7
β’
(meetβπΎ) =
(meetβπΎ) |
34 | 11, 33, 4, 12 | dihmeet 40306 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))) β
(BaseβπΎ) β§
((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) β
(BaseβπΎ)) β
(((DIsoHβπΎ)βπ)β((β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))(meetβπΎ)((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))))) =
((((DIsoHβπΎ)βπ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) β©
(((DIsoHβπΎ)βπ)β((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))))))) |
35 | 10, 27, 32, 34 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((DIsoHβπΎ)βπ)β((β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))(meetβπΎ)((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))))) =
((((DIsoHβπΎ)βπ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) β©
(((DIsoHβπΎ)βπ)β((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))))))) |
36 | | eqid 2732 |
. . . . . . . 8
β’
(0.βπΎ) =
(0.βπΎ) |
37 | 11, 30, 33, 36 | opnoncon 38170 |
. . . . . . 7
β’ ((πΎ β OP β§ (β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))) β
(BaseβπΎ)) β
((β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))(meetβπΎ)((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))))) =
(0.βπΎ)) |
38 | 29, 27, 37 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))(meetβπΎ)((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))))) =
(0.βπΎ)) |
39 | 38 | fveq2d 6895 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((DIsoHβπΎ)βπ)β((β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))(meetβπΎ)((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))))) =
(((DIsoHβπΎ)βπ)β(0.βπΎ))) |
40 | 35, 39 | eqtr3d 2774 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((((DIsoHβπΎ)βπ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) β©
(((DIsoHβπΎ)βπ)β((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))))) =
(((DIsoHβπΎ)βπ)β(0.βπΎ))) |
41 | 4, 12 | dihcnvid2 40236 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ( β₯ β( β₯
βπ)) β ran
((DIsoHβπΎ)βπ)) β (((DIsoHβπΎ)βπ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) = ( β₯
β( β₯ βπ))) |
42 | 25, 41 | syldan 591 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((DIsoHβπΎ)βπ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) = ( β₯
β( β₯ βπ))) |
43 | 30, 4, 12, 6 | dochvalr 40320 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ( β₯ β( β₯
βπ)) β ran
((DIsoHβπΎ)βπ)) β ( β₯ β( β₯
β( β₯ βπ))) = (((DIsoHβπΎ)βπ)β((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))))) |
44 | 25, 43 | syldan 591 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ β( β₯
β( β₯ βπ))) = (((DIsoHβπΎ)βπ)β((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))))) |
45 | 4, 12, 6 | dochoc 40330 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β ran ((DIsoHβπΎ)βπ)) β ( β₯ β( β₯
β( β₯ βπ))) = ( β₯ βπ)) |
46 | 19, 45 | syldan 591 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ β( β₯
β( β₯ βπ))) = ( β₯ βπ)) |
47 | 44, 46 | eqtr3d 2774 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((DIsoHβπΎ)βπ)β((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ))))) = ( β₯
βπ)) |
48 | 42, 47 | ineq12d 4213 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((((DIsoHβπΎ)βπ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))) β©
(((DIsoHβπΎ)βπ)β((ocβπΎ)β(β‘((DIsoHβπΎ)βπ)β( β₯ β( β₯
βπ)))))) = (( β₯
β( β₯ βπ)) β© ( β₯ βπ))) |
49 | | dochnoncon.z |
. . . . . 6
β’ 0 =
(0gβπ) |
50 | 36, 4, 12, 5, 49 | dih0 40243 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (((DIsoHβπΎ)βπ)β(0.βπΎ)) = { 0 }) |
51 | 50 | adantr 481 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((DIsoHβπΎ)βπ)β(0.βπΎ)) = { 0 }) |
52 | 40, 48, 51 | 3eqtr3d 2780 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (( β₯ β( β₯
βπ)) β© ( β₯
βπ)) = { 0
}) |
53 | 9, 52 | sseqtrd 4022 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π β© ( β₯ βπ)) β { 0 }) |
54 | 4, 5, 10 | dvhlmod 40073 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β LMod) |
55 | | simpr 485 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β π) |
56 | 4, 5, 12, 2 | dihrnlss 40240 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β ran ((DIsoHβπΎ)βπ)) β ( β₯ βπ) β π) |
57 | 19, 56 | syldan 591 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β π) |
58 | 2 | lssincl 20581 |
. . . 4
β’ ((π β LMod β§ π β π β§ ( β₯ βπ) β π) β (π β© ( β₯ βπ)) β π) |
59 | 54, 55, 57, 58 | syl3anc 1371 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π β© ( β₯ βπ)) β π) |
60 | 49, 2 | lss0ss 20564 |
. . 3
β’ ((π β LMod β§ (π β© ( β₯ βπ)) β π) β { 0 } β (π β© ( β₯ βπ))) |
61 | 54, 59, 60 | syl2anc 584 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β { 0 } β (π β© ( β₯ βπ))) |
62 | 53, 61 | eqssd 3999 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π β© ( β₯ βπ)) = { 0 }) |