Step | Hyp | Ref
| Expression |
1 | | dihjatcclem.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
2 | | dihjatcclem.h |
. . . 4
β’ π» = (LHypβπΎ) |
3 | | dihjatcclem.i |
. . . 4
β’ πΌ = ((DIsoHβπΎ)βπ) |
4 | 2, 3 | dihvalrel 40454 |
. . 3
β’ ((πΎ β HL β§ π β π») β Rel (πΌβπ)) |
5 | 1, 4 | syl 17 |
. 2
β’ (π β Rel (πΌβπ)) |
6 | 1 | adantr 480 |
. . . . . . 7
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β (πΎ β HL β§ π β π»)) |
7 | | dihjatcclem.l |
. . . . . . . . . . . 12
β’ β€ =
(leβπΎ) |
8 | | dihjatcclem.a |
. . . . . . . . . . . 12
β’ π΄ = (AtomsβπΎ) |
9 | | dihjatcc.w |
. . . . . . . . . . . 12
β’ πΆ = ((ocβπΎ)βπ) |
10 | 7, 8, 2, 9 | lhpocnel2 39194 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π») β (πΆ β π΄ β§ Β¬ πΆ β€ π)) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΆ β π΄ β§ Β¬ πΆ β€ π)) |
12 | | dihjatcclem.p |
. . . . . . . . . 10
β’ (π β (π β π΄ β§ Β¬ π β€ π)) |
13 | | dihjatcc.t |
. . . . . . . . . . 11
β’ π = ((LTrnβπΎ)βπ) |
14 | | dihjatcc.g |
. . . . . . . . . . 11
β’ πΊ = (β©π β π (πβπΆ) = π) |
15 | 7, 8, 2, 13, 14 | ltrniotacl 39754 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΆ β π΄ β§ Β¬ πΆ β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ β π) |
16 | 1, 11, 12, 15 | syl3anc 1370 |
. . . . . . . . 9
β’ (π β πΊ β π) |
17 | | dihjatcclem.q |
. . . . . . . . . . 11
β’ (π β (π β π΄ β§ Β¬ π β€ π)) |
18 | | dihjatcc.dd |
. . . . . . . . . . . 12
β’ π· = (β©π β π (πβπΆ) = π) |
19 | 7, 8, 2, 13, 18 | ltrniotacl 39754 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (πΆ β π΄ β§ Β¬ πΆ β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β π· β π) |
20 | 1, 11, 17, 19 | syl3anc 1370 |
. . . . . . . . . 10
β’ (π β π· β π) |
21 | 2, 13 | ltrncnv 39321 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π· β π) β β‘π· β π) |
22 | 1, 20, 21 | syl2anc 583 |
. . . . . . . . 9
β’ (π β β‘π· β π) |
23 | 2, 13 | ltrnco 39894 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ β‘π· β π) β (πΊ β β‘π·) β π) |
24 | 1, 16, 22, 23 | syl3anc 1370 |
. . . . . . . 8
β’ (π β (πΊ β β‘π·) β π) |
25 | 24 | adantr 480 |
. . . . . . 7
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β (πΊ β β‘π·) β π) |
26 | | simprll 776 |
. . . . . . 7
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β π β π) |
27 | | simprlr 777 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β (π
βπ) β€ π) |
28 | | dihjatcclem.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΎ) |
29 | | dihjatcclem.j |
. . . . . . . . . 10
β’ β¨ =
(joinβπΎ) |
30 | | dihjatcclem.m |
. . . . . . . . . 10
β’ β§ =
(meetβπΎ) |
31 | | dihjatcclem.u |
. . . . . . . . . 10
β’ π = ((DVecHβπΎ)βπ) |
32 | | dihjatcclem.s |
. . . . . . . . . 10
β’ β =
(LSSumβπ) |
33 | | dihjatcclem.v |
. . . . . . . . . 10
β’ π = ((π β¨ π) β§ π) |
34 | | dihjatcc.r |
. . . . . . . . . 10
β’ π
= ((trLβπΎ)βπ) |
35 | | dihjatcc.e |
. . . . . . . . . 10
β’ πΈ = ((TEndoβπΎ)βπ) |
36 | 28, 7, 2, 29, 30, 8, 31, 32, 3, 33, 1, 12, 17, 9, 13, 34, 35, 14, 18 | dihjatcclem3 40595 |
. . . . . . . . 9
β’ (π β (π
β(πΊ β β‘π·)) = π) |
37 | 36 | adantr 480 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β (π
β(πΊ β β‘π·)) = π) |
38 | 27, 37 | breqtrrd 5176 |
. . . . . . 7
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β (π
βπ) β€ (π
β(πΊ β β‘π·))) |
39 | 7, 2, 13, 34, 35 | tendoex 40150 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((πΊ β β‘π·) β π β§ π β π) β§ (π
βπ) β€ (π
β(πΊ β β‘π·))) β βπ‘ β πΈ (π‘β(πΊ β β‘π·)) = π) |
40 | 6, 25, 26, 38, 39 | syl121anc 1374 |
. . . . . 6
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β βπ‘ β πΈ (π‘β(πΊ β β‘π·)) = π) |
41 | | df-rex 3070 |
. . . . . 6
β’
(βπ‘ β
πΈ (π‘β(πΊ β β‘π·)) = π β βπ‘(π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) |
42 | 40, 41 | sylib 217 |
. . . . 5
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β βπ‘(π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) |
43 | | eqidd 2732 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (π‘βπΊ) = (π‘βπΊ)) |
44 | | simprl 768 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β π‘ β πΈ) |
45 | 1 | ad2antrr 723 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (πΎ β HL β§ π β π»)) |
46 | 12 | ad2antrr 723 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (π β π΄ β§ Β¬ π β€ π)) |
47 | | fvex 6904 |
. . . . . . . . . . . 12
β’ (π‘βπΊ) β V |
48 | | vex 3477 |
. . . . . . . . . . . 12
β’ π‘ β V |
49 | 7, 8, 2, 9, 13, 35, 3, 14, 47, 48 | dihopelvalcqat 40421 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (β¨(π‘βπΊ), π‘β© β (πΌβπ) β ((π‘βπΊ) = (π‘βπΊ) β§ π‘ β πΈ))) |
50 | 45, 46, 49 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (β¨(π‘βπΊ), π‘β© β (πΌβπ) β ((π‘βπΊ) = (π‘βπΊ) β§ π‘ β πΈ))) |
51 | 43, 44, 50 | mpbir2and 710 |
. . . . . . . . 9
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β β¨(π‘βπΊ), π‘β© β (πΌβπ)) |
52 | | eqidd 2732 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β ((πβπ‘)βπ·) = ((πβπ‘)βπ·)) |
53 | | dihjatcc.n |
. . . . . . . . . . . 12
β’ π = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) |
54 | 2, 13, 35, 53 | tendoicl 39971 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ) β (πβπ‘) β πΈ) |
55 | 45, 44, 54 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (πβπ‘) β πΈ) |
56 | 17 | ad2antrr 723 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (π β π΄ β§ Β¬ π β€ π)) |
57 | | fvex 6904 |
. . . . . . . . . . . 12
β’ ((πβπ‘)βπ·) β V |
58 | | fvex 6904 |
. . . . . . . . . . . 12
β’ (πβπ‘) β V |
59 | 7, 8, 2, 9, 13, 35, 3, 18, 57, 58 | dihopelvalcqat 40421 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ) β (((πβπ‘)βπ·) = ((πβπ‘)βπ·) β§ (πβπ‘) β πΈ))) |
60 | 45, 56, 59 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ) β (((πβπ‘)βπ·) = ((πβπ‘)βπ·) β§ (πβπ‘) β πΈ))) |
61 | 52, 55, 60 | mpbir2and 710 |
. . . . . . . . 9
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ)) |
62 | 16 | ad2antrr 723 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β πΊ β π) |
63 | 22 | ad2antrr 723 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β β‘π· β π) |
64 | 2, 13, 35 | tendospdi1 40195 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ πΊ β π β§ β‘π· β π)) β (π‘β(πΊ β β‘π·)) = ((π‘βπΊ) β (π‘ββ‘π·))) |
65 | 45, 44, 62, 63, 64 | syl13anc 1371 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (π‘β(πΊ β β‘π·)) = ((π‘βπΊ) β (π‘ββ‘π·))) |
66 | | simprr 770 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (π‘β(πΊ β β‘π·)) = π) |
67 | 20 | ad2antrr 723 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β π· β π) |
68 | 53, 13 | tendoi2 39970 |
. . . . . . . . . . . . 13
β’ ((π‘ β πΈ β§ π· β π) β ((πβπ‘)βπ·) = β‘(π‘βπ·)) |
69 | 44, 67, 68 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β ((πβπ‘)βπ·) = β‘(π‘βπ·)) |
70 | 2, 13, 35 | tendocnv 40196 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ β§ π· β π) β β‘(π‘βπ·) = (π‘ββ‘π·)) |
71 | 45, 44, 67, 70 | syl3anc 1370 |
. . . . . . . . . . . 12
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β β‘(π‘βπ·) = (π‘ββ‘π·)) |
72 | 69, 71 | eqtr2d 2772 |
. . . . . . . . . . 11
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (π‘ββ‘π·) = ((πβπ‘)βπ·)) |
73 | 72 | coeq2d 5862 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β ((π‘βπΊ) β (π‘ββ‘π·)) = ((π‘βπΊ) β ((πβπ‘)βπ·))) |
74 | 65, 66, 73 | 3eqtr3d 2779 |
. . . . . . . . 9
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β π = ((π‘βπΊ) β ((πβπ‘)βπ·))) |
75 | | simplrr 775 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β π = 0 ) |
76 | | dihjatcc.d |
. . . . . . . . . . . 12
β’ π½ = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) |
77 | | dihjatcc.o |
. . . . . . . . . . . 12
β’ 0 = (π β π β¦ ( I βΎ π΅)) |
78 | 2, 13, 35, 53, 28, 76, 77 | tendoipl2 39973 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ) β (π‘π½(πβπ‘)) = 0 ) |
79 | 45, 44, 78 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β (π‘π½(πβπ‘)) = 0 ) |
80 | 75, 79 | eqtr4d 2774 |
. . . . . . . . 9
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β π = (π‘π½(πβπ‘))) |
81 | | opeq1 4873 |
. . . . . . . . . . . . . . 15
β’ (π = (π‘βπΊ) β β¨π, π‘β© = β¨(π‘βπΊ), π‘β©) |
82 | 81 | eleq1d 2817 |
. . . . . . . . . . . . . 14
β’ (π = (π‘βπΊ) β (β¨π, π‘β© β (πΌβπ) β β¨(π‘βπΊ), π‘β© β (πΌβπ))) |
83 | 82 | anbi1d 629 |
. . . . . . . . . . . . 13
β’ (π = (π‘βπΊ) β ((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β (β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)))) |
84 | | coeq1 5857 |
. . . . . . . . . . . . . . 15
β’ (π = (π‘βπΊ) β (π β β) = ((π‘βπΊ) β β)) |
85 | 84 | eqeq2d 2742 |
. . . . . . . . . . . . . 14
β’ (π = (π‘βπΊ) β (π = (π β β) β π = ((π‘βπΊ) β β))) |
86 | 85 | anbi1d 629 |
. . . . . . . . . . . . 13
β’ (π = (π‘βπΊ) β ((π = (π β β) β§ π = (π‘π½π’)) β (π = ((π‘βπΊ) β β) β§ π = (π‘π½π’)))) |
87 | 83, 86 | anbi12d 630 |
. . . . . . . . . . . 12
β’ (π = (π‘βπΊ) β (((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))) β ((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β β) β§ π = (π‘π½π’))))) |
88 | | opeq1 4873 |
. . . . . . . . . . . . . . 15
β’ (β = ((πβπ‘)βπ·) β β¨β, π’β© = β¨((πβπ‘)βπ·), π’β©) |
89 | 88 | eleq1d 2817 |
. . . . . . . . . . . . . 14
β’ (β = ((πβπ‘)βπ·) β (β¨β, π’β© β (πΌβπ) β β¨((πβπ‘)βπ·), π’β© β (πΌβπ))) |
90 | 89 | anbi2d 628 |
. . . . . . . . . . . . 13
β’ (β = ((πβπ‘)βπ·) β ((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β (β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), π’β© β (πΌβπ)))) |
91 | | coeq2 5858 |
. . . . . . . . . . . . . . 15
β’ (β = ((πβπ‘)βπ·) β ((π‘βπΊ) β β) = ((π‘βπΊ) β ((πβπ‘)βπ·))) |
92 | 91 | eqeq2d 2742 |
. . . . . . . . . . . . . 14
β’ (β = ((πβπ‘)βπ·) β (π = ((π‘βπΊ) β β) β π = ((π‘βπΊ) β ((πβπ‘)βπ·)))) |
93 | 92 | anbi1d 629 |
. . . . . . . . . . . . 13
β’ (β = ((πβπ‘)βπ·) β ((π = ((π‘βπΊ) β β) β§ π = (π‘π½π’)) β (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½π’)))) |
94 | 90, 93 | anbi12d 630 |
. . . . . . . . . . . 12
β’ (β = ((πβπ‘)βπ·) β (((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β β) β§ π = (π‘π½π’))) β ((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), π’β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½π’))))) |
95 | | opeq2 4874 |
. . . . . . . . . . . . . . 15
β’ (π’ = (πβπ‘) β β¨((πβπ‘)βπ·), π’β© = β¨((πβπ‘)βπ·), (πβπ‘)β©) |
96 | 95 | eleq1d 2817 |
. . . . . . . . . . . . . 14
β’ (π’ = (πβπ‘) β (β¨((πβπ‘)βπ·), π’β© β (πΌβπ) β β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ))) |
97 | 96 | anbi2d 628 |
. . . . . . . . . . . . 13
β’ (π’ = (πβπ‘) β ((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), π’β© β (πΌβπ)) β (β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ)))) |
98 | | oveq2 7420 |
. . . . . . . . . . . . . . 15
β’ (π’ = (πβπ‘) β (π‘π½π’) = (π‘π½(πβπ‘))) |
99 | 98 | eqeq2d 2742 |
. . . . . . . . . . . . . 14
β’ (π’ = (πβπ‘) β (π = (π‘π½π’) β π = (π‘π½(πβπ‘)))) |
100 | 99 | anbi2d 628 |
. . . . . . . . . . . . 13
β’ (π’ = (πβπ‘) β ((π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½π’)) β (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½(πβπ‘))))) |
101 | 97, 100 | anbi12d 630 |
. . . . . . . . . . . 12
β’ (π’ = (πβπ‘) β (((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), π’β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½π’))) β ((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½(πβπ‘)))))) |
102 | 87, 94, 101 | syl3an9b 1433 |
. . . . . . . . . . 11
β’ ((π = (π‘βπΊ) β§ β = ((πβπ‘)βπ·) β§ π’ = (πβπ‘)) β (((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))) β ((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½(πβπ‘)))))) |
103 | 102 | spc3egv 3593 |
. . . . . . . . . 10
β’ (((π‘βπΊ) β V β§ ((πβπ‘)βπ·) β V β§ (πβπ‘) β V) β (((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½(πβπ‘)))) β βπβββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))))) |
104 | 47, 57, 58, 103 | mp3an 1460 |
. . . . . . . . 9
β’
(((β¨(π‘βπΊ), π‘β© β (πΌβπ) β§ β¨((πβπ‘)βπ·), (πβπ‘)β© β (πΌβπ)) β§ (π = ((π‘βπΊ) β ((πβπ‘)βπ·)) β§ π = (π‘π½(πβπ‘)))) β βπβββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’)))) |
105 | 51, 61, 74, 80, 104 | syl22anc 836 |
. . . . . . . 8
β’ (((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β§ (π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π)) β βπβββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’)))) |
106 | 105 | ex 412 |
. . . . . . 7
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β ((π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π) β βπβββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))))) |
107 | 106 | eximdv 1919 |
. . . . . 6
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β (βπ‘(π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π) β βπ‘βπβββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))))) |
108 | | excom 2161 |
. . . . . 6
β’
(βπ‘βπβββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’)))) |
109 | 107, 108 | imbitrdi 250 |
. . . . 5
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β (βπ‘(π‘ β πΈ β§ (π‘β(πΊ β β‘π·)) = π) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))))) |
110 | 42, 109 | mpd 15 |
. . . 4
β’ ((π β§ ((π β π β§ (π
βπ) β€ π) β§ π = 0 )) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’)))) |
111 | 110 | ex 412 |
. . 3
β’ (π β (((π β π β§ (π
βπ) β€ π) β§ π = 0 ) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))))) |
112 | 1 | simpld 494 |
. . . . . . . . 9
β’ (π β πΎ β HL) |
113 | 112 | hllatd 38538 |
. . . . . . . 8
β’ (π β πΎ β Lat) |
114 | 12 | simpld 494 |
. . . . . . . . 9
β’ (π β π β π΄) |
115 | 17 | simpld 494 |
. . . . . . . . 9
β’ (π β π β π΄) |
116 | 28, 29, 8 | hlatjcl 38541 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β π΅) |
117 | 112, 114,
115, 116 | syl3anc 1370 |
. . . . . . . 8
β’ (π β (π β¨ π) β π΅) |
118 | 1 | simprd 495 |
. . . . . . . . 9
β’ (π β π β π») |
119 | 28, 2 | lhpbase 39173 |
. . . . . . . . 9
β’ (π β π» β π β π΅) |
120 | 118, 119 | syl 17 |
. . . . . . . 8
β’ (π β π β π΅) |
121 | 28, 30 | latmcl 18398 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β ((π β¨ π) β§ π) β π΅) |
122 | 113, 117,
120, 121 | syl3anc 1370 |
. . . . . . 7
β’ (π β ((π β¨ π) β§ π) β π΅) |
123 | 33, 122 | eqeltrid 2836 |
. . . . . 6
β’ (π β π β π΅) |
124 | 28, 7, 30 | latmle2 18423 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β ((π β¨ π) β§ π) β€ π) |
125 | 113, 117,
120, 124 | syl3anc 1370 |
. . . . . . 7
β’ (π β ((π β¨ π) β§ π) β€ π) |
126 | 33, 125 | eqbrtrid 5183 |
. . . . . 6
β’ (π β π β€ π) |
127 | | eqid 2731 |
. . . . . . 7
β’
((DIsoBβπΎ)βπ) = ((DIsoBβπΎ)βπ) |
128 | 28, 7, 2, 3, 127 | dihvalb 40412 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = (((DIsoBβπΎ)βπ)βπ)) |
129 | 1, 123, 126, 128 | syl12anc 834 |
. . . . 5
β’ (π β (πΌβπ) = (((DIsoBβπΎ)βπ)βπ)) |
130 | 129 | eleq2d 2818 |
. . . 4
β’ (π β (β¨π, π β© β (πΌβπ) β β¨π, π β© β (((DIsoBβπΎ)βπ)βπ))) |
131 | 28, 7, 2, 13, 34, 77, 127 | dibopelval3 40323 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (β¨π, π β© β (((DIsoBβπΎ)βπ)βπ) β ((π β π β§ (π
βπ) β€ π) β§ π = 0 ))) |
132 | 1, 123, 126, 131 | syl12anc 834 |
. . . 4
β’ (π β (β¨π, π β© β (((DIsoBβπΎ)βπ)βπ) β ((π β π β§ (π
βπ) β€ π) β§ π = 0 ))) |
133 | 130, 132 | bitrd 279 |
. . 3
β’ (π β (β¨π, π β© β (πΌβπ) β ((π β π β§ (π
βπ) β€ π) β§ π = 0 ))) |
134 | | eqid 2731 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
135 | 28, 8 | atbase 38463 |
. . . . 5
β’ (π β π΄ β π β π΅) |
136 | 114, 135 | syl 17 |
. . . 4
β’ (π β π β π΅) |
137 | 28, 8 | atbase 38463 |
. . . . 5
β’ (π β π΄ β π β π΅) |
138 | 115, 137 | syl 17 |
. . . 4
β’ (π β π β π΅) |
139 | 28, 2, 13, 35, 76, 31, 134, 32, 3, 1, 136, 138 | dihopellsm 40430 |
. . 3
β’ (π β (β¨π, π β© β ((πΌβπ) β (πΌβπ)) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (π = (π β β) β§ π = (π‘π½π’))))) |
140 | 111, 133,
139 | 3imtr4d 294 |
. 2
β’ (π β (β¨π, π β© β (πΌβπ) β β¨π, π β© β ((πΌβπ) β (πΌβπ)))) |
141 | 5, 140 | relssdv 5788 |
1
β’ (π β (πΌβπ) β ((πΌβπ) β (πΌβπ))) |