Step | Hyp | Ref
| Expression |
1 | | djhcvat42.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
2 | 1 | simpld 495 |
. . 3
β’ (π β πΎ β HL) |
3 | | djhcvat42.s |
. . . 4
β’ (π β π β ran πΌ) |
4 | | eqid 2732 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
5 | | djhcvat42.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | | djhcvat42.i |
. . . . 5
β’ πΌ = ((DIsoHβπΎ)βπ) |
7 | 4, 5, 6 | dihcnvcl 40228 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β (BaseβπΎ)) |
8 | 1, 3, 7 | syl2anc 584 |
. . 3
β’ (π β (β‘πΌβπ) β (BaseβπΎ)) |
9 | | djhcvat42.x |
. . . . 5
β’ (π β π β (π β { 0 })) |
10 | 9 | eldifad 3960 |
. . . 4
β’ (π β π β π) |
11 | | eldifsni 4793 |
. . . . 5
β’ (π β (π β { 0 }) β π β 0 ) |
12 | 9, 11 | syl 17 |
. . . 4
β’ (π β π β 0 ) |
13 | | eqid 2732 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
14 | | djhcvat42.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
15 | | djhcvat42.v |
. . . . 5
β’ π = (Baseβπ) |
16 | | djhcvat42.o |
. . . . 5
β’ 0 =
(0gβπ) |
17 | | djhcvat42.n |
. . . . 5
β’ π = (LSpanβπ) |
18 | 13, 5, 14, 15, 16, 17, 6 | dihlspsnat 40290 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (β‘πΌβ(πβ{π})) β (AtomsβπΎ)) |
19 | 1, 10, 12, 18 | syl3anc 1371 |
. . 3
β’ (π β (β‘πΌβ(πβ{π})) β (AtomsβπΎ)) |
20 | | djhcvat42.y |
. . . . 5
β’ (π β π β (π β { 0 })) |
21 | 20 | eldifad 3960 |
. . . 4
β’ (π β π β π) |
22 | | eldifsni 4793 |
. . . . 5
β’ (π β (π β { 0 }) β π β 0 ) |
23 | 20, 22 | syl 17 |
. . . 4
β’ (π β π β 0 ) |
24 | 13, 5, 14, 15, 16, 17, 6 | dihlspsnat 40290 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (β‘πΌβ(πβ{π})) β (AtomsβπΎ)) |
25 | 1, 21, 23, 24 | syl3anc 1371 |
. . 3
β’ (π β (β‘πΌβ(πβ{π})) β (AtomsβπΎ)) |
26 | | eqid 2732 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
27 | | eqid 2732 |
. . . 4
β’
(joinβπΎ) =
(joinβπΎ) |
28 | | eqid 2732 |
. . . 4
β’
(0.βπΎ) =
(0.βπΎ) |
29 | 4, 26, 27, 28, 13 | cvrat42 38401 |
. . 3
β’ ((πΎ β HL β§ ((β‘πΌβπ) β (BaseβπΎ) β§ (β‘πΌβ(πβ{π})) β (AtomsβπΎ) β§ (β‘πΌβ(πβ{π})) β (AtomsβπΎ))) β (((β‘πΌβπ) β (0.βπΎ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβπ)(joinβπΎ)(β‘πΌβ(πβ{π})))) β βπ β (AtomsβπΎ)(π(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)(π(joinβπΎ)(β‘πΌβ(πβ{π})))))) |
30 | 2, 8, 19, 25, 29 | syl13anc 1372 |
. 2
β’ (π β (((β‘πΌβπ) β (0.βπΎ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβπ)(joinβπΎ)(β‘πΌβ(πβ{π})))) β βπ β (AtomsβπΎ)(π(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)(π(joinβπΎ)(β‘πΌβ(πβ{π})))))) |
31 | 5, 28, 6, 14, 15, 16, 17, 1, 3 | dih0sb 40242 |
. . . 4
β’ (π β (π = { 0 } β (β‘πΌβπ) = (0.βπΎ))) |
32 | 31 | necon3bid 2985 |
. . 3
β’ (π β (π β { 0 } β (β‘πΌβπ) β (0.βπΎ))) |
33 | 5, 14, 15, 17, 6 | dihlsprn 40288 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran πΌ) |
34 | 1, 10, 33 | syl2anc 584 |
. . . . 5
β’ (π β (πβ{π}) β ran πΌ) |
35 | 5, 14, 6, 15 | dihrnss 40235 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β π) |
36 | 1, 3, 35 | syl2anc 584 |
. . . . . 6
β’ (π β π β π) |
37 | 5, 14, 15, 17, 6 | dihlsprn 40288 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran πΌ) |
38 | 1, 21, 37 | syl2anc 584 |
. . . . . . 7
β’ (π β (πβ{π}) β ran πΌ) |
39 | 5, 14, 6, 15 | dihrnss 40235 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πβ{π}) β ran πΌ) β (πβ{π}) β π) |
40 | 1, 38, 39 | syl2anc 584 |
. . . . . 6
β’ (π β (πβ{π}) β π) |
41 | | djhcvat42.j |
. . . . . . 7
β’ β¨ =
((joinHβπΎ)βπ) |
42 | 5, 6, 14, 15, 41 | djhcl 40357 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ (πβ{π}) β π)) β (π β¨ (πβ{π})) β ran πΌ) |
43 | 1, 36, 40, 42 | syl12anc 835 |
. . . . 5
β’ (π β (π β¨ (πβ{π})) β ran πΌ) |
44 | 26, 5, 6, 1, 34, 43 | dihcnvord 40231 |
. . . 4
β’ (π β ((β‘πΌβ(πβ{π}))(leβπΎ)(β‘πΌβ(π β¨ (πβ{π}))) β (πβ{π}) β (π β¨ (πβ{π})))) |
45 | 27, 5, 6, 41, 1, 3,
38 | djhj 40361 |
. . . . 5
β’ (π β (β‘πΌβ(π β¨ (πβ{π}))) = ((β‘πΌβπ)(joinβπΎ)(β‘πΌβ(πβ{π})))) |
46 | 45 | breq2d 5160 |
. . . 4
β’ (π β ((β‘πΌβ(πβ{π}))(leβπΎ)(β‘πΌβ(π β¨ (πβ{π}))) β (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβπ)(joinβπΎ)(β‘πΌβ(πβ{π}))))) |
47 | 44, 46 | bitr3d 280 |
. . 3
β’ (π β ((πβ{π}) β (π β¨ (πβ{π})) β (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβπ)(joinβπΎ)(β‘πΌβ(πβ{π}))))) |
48 | 32, 47 | anbi12d 631 |
. 2
β’ (π β ((π β { 0 } β§ (πβ{π}) β (π β¨ (πβ{π}))) β ((β‘πΌβπ) β (0.βπΎ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβπ)(joinβπΎ)(β‘πΌβ(πβ{π})))))) |
49 | 1 | adantr 481 |
. . . . 5
β’ ((π β§ π§ β (π β { 0 })) β (πΎ β HL β§ π β π»)) |
50 | | eldifi 4126 |
. . . . . 6
β’ (π§ β (π β { 0 }) β π§ β π) |
51 | 50 | adantl 482 |
. . . . 5
β’ ((π β§ π§ β (π β { 0 })) β π§ β π) |
52 | | eldifsni 4793 |
. . . . . 6
β’ (π§ β (π β { 0 }) β π§ β 0 ) |
53 | 52 | adantl 482 |
. . . . 5
β’ ((π β§ π§ β (π β { 0 })) β π§ β 0 ) |
54 | 13, 5, 14, 15, 16, 17, 6 | dihlspsnat 40290 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π§ β π β§ π§ β 0 ) β (β‘πΌβ(πβ{π§})) β (AtomsβπΎ)) |
55 | 49, 51, 53, 54 | syl3anc 1371 |
. . . 4
β’ ((π β§ π§ β (π β { 0 })) β (β‘πΌβ(πβ{π§})) β (AtomsβπΎ)) |
56 | 13, 5, 14, 15, 16, 17, 6, 1 | dihatexv2 40296 |
. . . 4
β’ (π β (π β (AtomsβπΎ) β βπ§ β (π β { 0 })π = (β‘πΌβ(πβ{π§})))) |
57 | | breq1 5151 |
. . . . . 6
β’ (π = (β‘πΌβ(πβ{π§})) β (π(leβπΎ)(β‘πΌβπ) β (β‘πΌβ(πβ{π§}))(leβπΎ)(β‘πΌβπ))) |
58 | | oveq1 7418 |
. . . . . . 7
β’ (π = (β‘πΌβ(πβ{π§})) β (π(joinβπΎ)(β‘πΌβ(πβ{π}))) = ((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π})))) |
59 | 58 | breq2d 5160 |
. . . . . 6
β’ (π = (β‘πΌβ(πβ{π§})) β ((β‘πΌβ(πβ{π}))(leβπΎ)(π(joinβπΎ)(β‘πΌβ(πβ{π}))) β (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π}))))) |
60 | 57, 59 | anbi12d 631 |
. . . . 5
β’ (π = (β‘πΌβ(πβ{π§})) β ((π(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)(π(joinβπΎ)(β‘πΌβ(πβ{π})))) β ((β‘πΌβ(πβ{π§}))(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π})))))) |
61 | 60 | adantl 482 |
. . . 4
β’ ((π β§ π = (β‘πΌβ(πβ{π§}))) β ((π(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)(π(joinβπΎ)(β‘πΌβ(πβ{π})))) β ((β‘πΌβ(πβ{π§}))(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π})))))) |
62 | 55, 56, 61 | rexxfr2d 5409 |
. . 3
β’ (π β (βπ β (AtomsβπΎ)(π(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)(π(joinβπΎ)(β‘πΌβ(πβ{π})))) β βπ§ β (π β { 0 })((β‘πΌβ(πβ{π§}))(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π})))))) |
63 | 5, 14, 15, 17, 6 | dihlsprn 40288 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π§ β π) β (πβ{π§}) β ran πΌ) |
64 | 49, 51, 63 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π§ β (π β { 0 })) β (πβ{π§}) β ran πΌ) |
65 | 3 | adantr 481 |
. . . . . 6
β’ ((π β§ π§ β (π β { 0 })) β π β ran πΌ) |
66 | 26, 5, 6, 49, 64, 65 | dihcnvord 40231 |
. . . . 5
β’ ((π β§ π§ β (π β { 0 })) β ((β‘πΌβ(πβ{π§}))(leβπΎ)(β‘πΌβπ) β (πβ{π§}) β π)) |
67 | 38 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π§ β (π β { 0 })) β (πβ{π}) β ran πΌ) |
68 | 27, 5, 6, 41, 49, 64, 67 | djhj 40361 |
. . . . . . 7
β’ ((π β§ π§ β (π β { 0 })) β (β‘πΌβ((πβ{π§}) β¨ (πβ{π}))) = ((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π})))) |
69 | 68 | breq2d 5160 |
. . . . . 6
β’ ((π β§ π§ β (π β { 0 })) β ((β‘πΌβ(πβ{π}))(leβπΎ)(β‘πΌβ((πβ{π§}) β¨ (πβ{π}))) β (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π}))))) |
70 | 10 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π§ β (π β { 0 })) β π β π) |
71 | 49, 70, 33 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π§ β (π β { 0 })) β (πβ{π}) β ran πΌ) |
72 | 5, 14, 6, 15 | dihrnss 40235 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πβ{π§}) β ran πΌ) β (πβ{π§}) β π) |
73 | 49, 64, 72 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ π§ β (π β { 0 })) β (πβ{π§}) β π) |
74 | 40 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π§ β (π β { 0 })) β (πβ{π}) β π) |
75 | 5, 6, 14, 15, 41 | djhcl 40357 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((πβ{π§}) β π β§ (πβ{π}) β π)) β ((πβ{π§}) β¨ (πβ{π})) β ran πΌ) |
76 | 49, 73, 74, 75 | syl12anc 835 |
. . . . . . 7
β’ ((π β§ π§ β (π β { 0 })) β ((πβ{π§}) β¨ (πβ{π})) β ran πΌ) |
77 | 26, 5, 6, 49, 71, 76 | dihcnvord 40231 |
. . . . . 6
β’ ((π β§ π§ β (π β { 0 })) β ((β‘πΌβ(πβ{π}))(leβπΎ)(β‘πΌβ((πβ{π§}) β¨ (πβ{π}))) β (πβ{π}) β ((πβ{π§}) β¨ (πβ{π})))) |
78 | 69, 77 | bitr3d 280 |
. . . . 5
β’ ((π β§ π§ β (π β { 0 })) β ((β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π}))) β (πβ{π}) β ((πβ{π§}) β¨ (πβ{π})))) |
79 | 66, 78 | anbi12d 631 |
. . . 4
β’ ((π β§ π§ β (π β { 0 })) β (((β‘πΌβ(πβ{π§}))(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π})))) β ((πβ{π§}) β π β§ (πβ{π}) β ((πβ{π§}) β¨ (πβ{π}))))) |
80 | 79 | rexbidva 3176 |
. . 3
β’ (π β (βπ§ β (π β { 0 })((β‘πΌβ(πβ{π§}))(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)((β‘πΌβ(πβ{π§}))(joinβπΎ)(β‘πΌβ(πβ{π})))) β βπ§ β (π β { 0 })((πβ{π§}) β π β§ (πβ{π}) β ((πβ{π§}) β¨ (πβ{π}))))) |
81 | 62, 80 | bitr2d 279 |
. 2
β’ (π β (βπ§ β (π β { 0 })((πβ{π§}) β π β§ (πβ{π}) β ((πβ{π§}) β¨ (πβ{π}))) β βπ β (AtomsβπΎ)(π(leβπΎ)(β‘πΌβπ) β§ (β‘πΌβ(πβ{π}))(leβπΎ)(π(joinβπΎ)(β‘πΌβ(πβ{π})))))) |
82 | 30, 48, 81 | 3imtr4d 293 |
1
β’ (π β ((π β { 0 } β§ (πβ{π}) β (π β¨ (πβ{π}))) β βπ§ β (π β { 0 })((πβ{π§}) β π β§ (πβ{π}) β ((πβ{π§}) β¨ (πβ{π}))))) |