Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (πΎ β HL β§ π β π»)) |
2 | | cdleml6.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
3 | | cdleml6.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
4 | | cdleml6.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
5 | | cdleml6.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
6 | | cdleml6.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
7 | | cdleml6.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
8 | | cdleml6.p |
. . . . . 6
β’ π = ((ocβπΎ)βπ) |
9 | | cdleml6.z |
. . . . . 6
β’ π = ((π β¨ (π
βπ)) β§ ((ββπ) β¨ (π
β(π β β‘(π ββ))))) |
10 | | cdleml6.y |
. . . . . 6
β’ π = ((π β¨ (π
βπ)) β§ (π β¨ (π
β(π β β‘π)))) |
11 | | cdleml6.x |
. . . . . 6
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
β(π ββ)) β§ (π
βπ) β (π
βπ)) β (π§βπ) = π)) |
12 | | cdleml6.u |
. . . . . 6
β’ π = (π β π β¦ if((π ββ) = β, π, π)) |
13 | | cdleml6.e |
. . . . . 6
β’ πΈ = ((TEndoβπΎ)βπ) |
14 | | cdleml6.o |
. . . . . 6
β’ 0 = (π β π β¦ ( I βΎ π΅)) |
15 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cdleml6 39447 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β (π β πΈ β§ (πβ(π ββ)) = β)) |
16 | 15 | 3adant2r 1180 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (π β πΈ β§ (πβ(π ββ)) = β)) |
17 | 16 | simpld 496 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β π β πΈ) |
18 | | simp3l 1202 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β π β πΈ) |
19 | 5, 13 | tendococl 39238 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π ) β πΈ) |
20 | 1, 17, 18, 19 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (π β π ) β πΈ) |
21 | 5, 6, 13 | tendoidcl 39235 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |
22 | 21 | 3ad2ant1 1134 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β ( I βΎ
π) β πΈ) |
23 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cdleml7 39448 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β ((π β π )ββ) = (( I βΎ π)ββ)) |
24 | 23 | 3adant2r 1180 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β ((π β π )ββ) = (( I βΎ π)ββ)) |
25 | | simp2 1138 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (β β π β§ β β ( I βΎ π΅))) |
26 | 2, 5, 6, 13 | tendocan 39290 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π ) β πΈ β§ ( I βΎ π) β πΈ β§ ((π β π )ββ) = (( I βΎ π)ββ)) β§ (β β π β§ β β ( I βΎ π΅))) β (π β π ) = ( I βΎ π)) |
27 | 1, 20, 22, 24, 25, 26 | syl131anc 1384 |
1
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (π β π ) = ( I βΎ π)) |