Step | Hyp | Ref
| Expression |
1 | | cdlemk3.x |
. 2
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β π§ = (πππΊ))) |
2 | | fveq1 6887 |
. . . . . . . . 9
β’ (π§ = (πππΊ) β (π§βπ) = ((πππΊ)βπ)) |
3 | | simpll1 1212 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β (πΎ β HL β§ π β π»)) |
4 | | simplr1 1215 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β π§ β π) |
5 | | simpl1 1191 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΎ β HL β§ π β π»)) |
6 | | simpl3r 1229 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπΉ) = (π
βπ)) |
7 | | simp22l 1292 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β πΊ β π) |
8 | 7 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΊ β π) |
9 | 5, 6, 8 | 3jca 1128 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π)) |
10 | 9 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β ((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π)) |
11 | | simp21l 1290 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β πΉ β π) |
12 | 11 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΉ β π) |
13 | | simpr2 1195 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π) |
14 | | simpl23 1253 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π) |
15 | 12, 13, 14 | 3jca 1128 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΉ β π β§ π β π β§ π β π)) |
16 | 15 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β (πΉ β π β§ π β π β§ π β π)) |
17 | | simpr32 1264 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπ) β (π
βπΉ)) |
18 | | simpr33 1265 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπ) β (π
βπΊ)) |
19 | 17, 18 | jca 512 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ))) |
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β ((π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ))) |
21 | | simp21r 1291 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β πΉ β ( I βΎ π΅)) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΉ β ( I βΎ π΅)) |
23 | | simp22r 1293 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β πΊ β ( I βΎ π΅)) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΊ β ( I βΎ π΅)) |
25 | | simpr31 1263 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β ( I βΎ π΅)) |
26 | 22, 24, 25 | 3jca 1128 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅))) |
27 | 26 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅))) |
28 | | simpl3l 1228 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π β π΄ β§ Β¬ π β€ π)) |
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β (π β π΄ β§ Β¬ π β€ π)) |
30 | | cdlemk3.b |
. . . . . . . . . . . . 13
β’ π΅ = (BaseβπΎ) |
31 | | cdlemk3.l |
. . . . . . . . . . . . 13
β’ β€ =
(leβπΎ) |
32 | | cdlemk3.j |
. . . . . . . . . . . . 13
β’ β¨ =
(joinβπΎ) |
33 | | cdlemk3.m |
. . . . . . . . . . . . 13
β’ β§ =
(meetβπΎ) |
34 | | cdlemk3.a |
. . . . . . . . . . . . 13
β’ π΄ = (AtomsβπΎ) |
35 | | cdlemk3.h |
. . . . . . . . . . . . 13
β’ π» = (LHypβπΎ) |
36 | | cdlemk3.t |
. . . . . . . . . . . . 13
β’ π = ((LTrnβπΎ)βπ) |
37 | | cdlemk3.r |
. . . . . . . . . . . . 13
β’ π
= ((trLβπΎ)βπ) |
38 | | cdlemk3.s |
. . . . . . . . . . . . 13
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))))) |
39 | | cdlemk3.u1 |
. . . . . . . . . . . . 13
β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘π)))))) |
40 | 30, 31, 32, 33, 34, 35, 36, 37, 38, 39 | cdlemkuel-3 39757 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π) β§ (πΉ β π β§ π β π β§ π β π) β§ (((π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πππΊ) β π) |
41 | 10, 16, 20, 27, 29, 40 | syl113anc 1382 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β (πππΊ) β π) |
42 | | simpr 485 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β (π§βπ) = ((πππΊ)βπ)) |
43 | 31, 34, 35, 36 | cdlemd 39066 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ π§ β π β§ (πππΊ) β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π§βπ) = ((πππΊ)βπ)) β π§ = (πππΊ)) |
44 | 3, 4, 41, 29, 42, 43 | syl311anc 1384 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β§ (π§βπ) = ((πππΊ)βπ)) β π§ = (πππΊ)) |
45 | 44 | ex 413 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((π§βπ) = ((πππΊ)βπ) β π§ = (πππΊ))) |
46 | 2, 45 | impbid2 225 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π§ = (πππΊ) β (π§βπ) = ((πππΊ)βπ))) |
47 | | simp1 1136 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β (πΎ β HL β§ π β π»)) |
48 | | simp3r 1202 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β (π
βπΉ) = (π
βπ)) |
49 | 47, 48 | jca 512 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β ((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ))) |
50 | 49 | adantr 481 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ))) |
51 | 22, 25, 24 | 3jca 1128 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅))) |
52 | 30, 31, 32, 33, 34, 35, 36, 37, 38, 39 | cdlemk32 39756 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ π β π β§ π β π) β§ πΊ β π) β§ (((π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πππΊ)βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))) |
53 | 50, 15, 8, 19, 51, 28, 52 | syl123anc 1387 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((πππΊ)βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))) |
54 | 53 | eqeq2d 2743 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((π§βπ) = ((πππΊ)βπ) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π)))))) |
55 | 46, 54 | bitrd 278 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ (π§ β π β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π§ = (πππΊ) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π)))))) |
56 | 55 | 3exp2 1354 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β (π§ β π β (π β π β ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β (π§ = (πππΊ) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))))))) |
57 | 56 | imp31 418 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ π§ β π) β§ π β π) β ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β (π§ = (πππΊ) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))))) |
58 | 57 | pm5.74d 272 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ π§ β π) β§ π β π) β (((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β π§ = (πππΊ)) β ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))))) |
59 | 58 | ralbidva 3175 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β§ π§ β π) β (βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β π§ = (πππΊ)) β βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))))) |
60 | 59 | riotabidva 7381 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β π§ = (πππΊ))) = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))))) |
61 | 1, 60 | eqtrid 2784 |
1
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β (π§βπ) = ((π β¨ (π
βπΊ)) β§ (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
β(πΊ β β‘π))))))) |