Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β π β€ π) |
2 | | simpl1 1191 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β πΎ β HL) |
3 | | simpl3 1193 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β π β π) |
4 | | llncvrlpln2.n |
. . . . . 6
β’ π = (LLinesβπΎ) |
5 | | llncvrlpln2.p |
. . . . . 6
β’ π = (LPlanesβπΎ) |
6 | 4, 5 | lplnnelln 37600 |
. . . . 5
β’ ((πΎ β HL β§ π β π) β Β¬ π β π) |
7 | 2, 3, 6 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β Β¬ π β π) |
8 | | simpl2 1192 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β π β π) |
9 | | eleq1 2824 |
. . . . . 6
β’ (π = π β (π β π β π β π)) |
10 | 8, 9 | syl5ibcom 246 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β (π = π β π β π)) |
11 | 10 | necon3bd 2955 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β (Β¬ π β π β π β π)) |
12 | 7, 11 | mpd 15 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β π β π) |
13 | | llncvrlpln2.l |
. . . . 5
β’ β€ =
(leβπΎ) |
14 | | eqid 2736 |
. . . . 5
β’
(ltβπΎ) =
(ltβπΎ) |
15 | 13, 14 | pltval 18092 |
. . . 4
β’ ((πΎ β HL β§ π β π β§ π β π) β (π(ltβπΎ)π β (π β€ π β§ π β π))) |
16 | 15 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β (π(ltβπΎ)π β (π β€ π β§ π β π))) |
17 | 1, 12, 16 | mpbir2and 711 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β π(ltβπΎ)π) |
18 | | simpl1 1191 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β πΎ β HL) |
19 | | simpl2 1192 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β π β π) |
20 | | eqid 2736 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
21 | 20, 4 | llnbase 37563 |
. . . . 5
β’ (π β π β π β (BaseβπΎ)) |
22 | 19, 21 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β π β (BaseβπΎ)) |
23 | | simpl3 1193 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β π β π) |
24 | 20, 5 | lplnbase 37588 |
. . . . 5
β’ (π β π β π β (BaseβπΎ)) |
25 | 23, 24 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β π β (BaseβπΎ)) |
26 | | simpr 486 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β π(ltβπΎ)π) |
27 | | eqid 2736 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
28 | | llncvrlpln2.c |
. . . . 5
β’ πΆ = ( β βπΎ) |
29 | | eqid 2736 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
30 | 20, 13, 14, 27, 28, 29 | hlrelat3 37466 |
. . . 4
β’ (((πΎ β HL β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ π(ltβπΎ)π) β βπ β (AtomsβπΎ)(ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) |
31 | 18, 22, 25, 26, 30 | syl31anc 1373 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β βπ β (AtomsβπΎ)(ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) |
32 | 20, 13, 27, 29, 5 | islpln2 37590 |
. . . . . . . 8
β’ (πΎ β HL β (π β π β (π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ‘ β (AtomsβπΎ)βπ’ β (AtomsβπΎ)(π β π‘ β§ Β¬ π’ β€ (π (joinβπΎ)π‘) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’))))) |
33 | 32 | adantr 482 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π) β (π β π β (π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ‘ β (AtomsβπΎ)βπ’ β (AtomsβπΎ)(π β π‘ β§ Β¬ π’ β€ (π (joinβπΎ)π‘) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’))))) |
34 | | simp3 1138 |
. . . . . . . . . . 11
β’ ((π β π‘ β§ Β¬ π’ β€ (π (joinβπΎ)π‘) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’)) β π = ((π (joinβπΎ)π‘)(joinβπΎ)π’)) |
35 | 20, 27, 29, 4 | islln2 37565 |
. . . . . . . . . . . . 13
β’ (πΎ β HL β (π β π β (π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π))))) |
36 | | simp3l 1201 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β ππΆ(π(joinβπΎ)π)) |
37 | | simp3r 1202 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (π(joinβπΎ)π) β€ π) |
38 | | simp12r 1287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π = (π(joinβπΎ)π)) |
39 | 38 | oveq1d 7319 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (π(joinβπΎ)π) = ((π(joinβπΎ)π)(joinβπΎ)π)) |
40 | | simp22 1207 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π = ((π (joinβπΎ)π‘)(joinβπΎ)π’)) |
41 | 37, 39, 40 | 3brtr3d 5113 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β ((π(joinβπΎ)π)(joinβπΎ)π) β€ ((π (joinβπΎ)π‘)(joinβπΎ)π’)) |
42 | | simp111 1302 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β πΎ β HL) |
43 | | simp112 1303 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π β (AtomsβπΎ)) |
44 | | simp113 1304 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π β (AtomsβπΎ)) |
45 | | simp23 1208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π β (AtomsβπΎ)) |
46 | 43, 44, 45 | 3jca 1128 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (π β (AtomsβπΎ) β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) |
47 | | simp13l 1288 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π β (AtomsβπΎ)) |
48 | | simp13r 1289 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π‘ β (AtomsβπΎ)) |
49 | | simp21 1206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π’ β (AtomsβπΎ)) |
50 | 47, 48, 49 | 3jca 1128 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ) β§ π’ β (AtomsβπΎ))) |
51 | 36, 38, 39 | 3brtr3d 5113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (π(joinβπΎ)π)πΆ((π(joinβπΎ)π)(joinβπΎ)π)) |
52 | 20, 27, 29 | hlatjcl 37421 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π(joinβπΎ)π) β (BaseβπΎ)) |
53 | 42, 43, 44, 52 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (π(joinβπΎ)π) β (BaseβπΎ)) |
54 | 20, 13, 27, 28, 29 | cvr1 37464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΎ β HL β§ (π(joinβπΎ)π) β (BaseβπΎ) β§ π β (AtomsβπΎ)) β (Β¬ π β€ (π(joinβπΎ)π) β (π(joinβπΎ)π)πΆ((π(joinβπΎ)π)(joinβπΎ)π))) |
55 | 42, 53, 45, 54 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (Β¬ π β€ (π(joinβπΎ)π) β (π(joinβπΎ)π)πΆ((π(joinβπΎ)π)(joinβπΎ)π))) |
56 | 51, 55 | mpbird 258 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β Β¬ π β€ (π(joinβπΎ)π)) |
57 | | simp12l 1286 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β π β π) |
58 | 13, 27, 29 | 3at 37544 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ) β§ π’ β (AtomsβπΎ))) β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β π)) β (((π(joinβπΎ)π)(joinβπΎ)π) β€ ((π (joinβπΎ)π‘)(joinβπΎ)π’) β ((π(joinβπΎ)π)(joinβπΎ)π) = ((π (joinβπΎ)π‘)(joinβπΎ)π’))) |
59 | 42, 46, 50, 56, 57, 58 | syl32anc 1378 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (((π(joinβπΎ)π)(joinβπΎ)π) β€ ((π (joinβπΎ)π‘)(joinβπΎ)π’) β ((π(joinβπΎ)π)(joinβπΎ)π) = ((π (joinβπΎ)π‘)(joinβπΎ)π’))) |
60 | 41, 59 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β ((π(joinβπΎ)π)(joinβπΎ)π) = ((π (joinβπΎ)π‘)(joinβπΎ)π’)) |
61 | 60, 39, 40 | 3eqtr4d 2786 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β (π(joinβπΎ)π) = π) |
62 | 36, 61 | breqtrd 5108 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β§ (π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β§ (ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β ππΆπ) |
63 | 62 | 3exp 1119 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β ((π’ β (AtomsβπΎ) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β§ π β (AtomsβπΎ)) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))) |
64 | 63 | 3expd 1353 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π)) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β (π’ β (AtomsβπΎ) β (π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))))) |
65 | 64 | 3exp 1119 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β ((π β π β§ π = (π(joinβπΎ)π)) β ((π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ)) β (π’ β (AtomsβπΎ) β (π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))))))) |
66 | 65 | 3expib 1122 |
. . . . . . . . . . . . . . 15
β’ (πΎ β HL β ((π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β ((π β π β§ π = (π(joinβπΎ)π)) β ((π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ)) β (π’ β (AtomsβπΎ) β (π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ)))))))) |
67 | 66 | rexlimdvv 3201 |
. . . . . . . . . . . . . 14
β’ (πΎ β HL β (βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π)) β ((π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ)) β (π’ β (AtomsβπΎ) β (π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))))))) |
68 | 67 | adantld 492 |
. . . . . . . . . . . . 13
β’ (πΎ β HL β ((π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π))) β ((π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ)) β (π’ β (AtomsβπΎ) β (π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))))))) |
69 | 35, 68 | sylbid 240 |
. . . . . . . . . . . 12
β’ (πΎ β HL β (π β π β ((π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ)) β (π’ β (AtomsβπΎ) β (π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))))))) |
70 | 69 | imp31 419 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β (π’ β (AtomsβπΎ) β (π = ((π (joinβπΎ)π‘)(joinβπΎ)π’) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))))) |
71 | 34, 70 | syl7 74 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β (π’ β (AtomsβπΎ) β ((π β π‘ β§ Β¬ π’ β€ (π (joinβπΎ)π‘) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’)) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))))) |
72 | 71 | rexlimdv 3147 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π) β§ (π β (AtomsβπΎ) β§ π‘ β (AtomsβπΎ))) β (βπ’ β (AtomsβπΎ)(π β π‘ β§ Β¬ π’ β€ (π (joinβπΎ)π‘) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’)) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ)))) |
73 | 72 | rexlimdvva 3202 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π) β (βπ β (AtomsβπΎ)βπ‘ β (AtomsβπΎ)βπ’ β (AtomsβπΎ)(π β π‘ β§ Β¬ π’ β€ (π (joinβπΎ)π‘) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’)) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ)))) |
74 | 73 | adantld 492 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π) β ((π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ‘ β (AtomsβπΎ)βπ’ β (AtomsβπΎ)(π β π‘ β§ Β¬ π’ β€ (π (joinβπΎ)π‘) β§ π = ((π (joinβπΎ)π‘)(joinβπΎ)π’))) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ)))) |
75 | 33, 74 | sylbid 240 |
. . . . . 6
β’ ((πΎ β HL β§ π β π) β (π β π β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ)))) |
76 | 75 | 3impia 1117 |
. . . . 5
β’ ((πΎ β HL β§ π β π β§ π β π) β (π β (AtomsβπΎ) β ((ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ))) |
77 | 76 | rexlimdv 3147 |
. . . 4
β’ ((πΎ β HL β§ π β π β§ π β π) β (βπ β (AtomsβπΎ)(ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β ππΆπ)) |
78 | 77 | imp 408 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ βπ β (AtomsβπΎ)(ππΆ(π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π)) β ππΆπ) |
79 | 31, 78 | syldan 592 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π(ltβπΎ)π) β ππΆπ) |
80 | 17, 79 | syldan 592 |
1
β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β ππΆπ) |