Step | Hyp | Ref
| Expression |
1 | | islpln5.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | islpln5.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | islpln5.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | islpln5.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
5 | | eqid 2737 |
. . 3
β’
(LLinesβπΎ) =
(LLinesβπΎ) |
6 | | islpln5.p |
. . 3
β’ π = (LPlanesβπΎ) |
7 | 1, 2, 3, 4, 5, 6 | islpln3 38025 |
. 2
β’ ((πΎ β HL β§ π β π΅) β (π β π β βπ¦ β (LLinesβπΎ)βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) |
8 | | df-rex 3075 |
. . 3
β’
(βπ¦ β
(LLinesβπΎ)βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)) β βπ¦(π¦ β (LLinesβπΎ) β§ βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) |
9 | | r19.41v 3186 |
. . . . . . . . . 10
β’
(βπ β
π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β (βπ β π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
10 | | an13 646 |
. . . . . . . . . 10
β’
((βπ β
π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β (π¦ = (π β¨ π) β§ (π β π β§ βπ β π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))))) |
11 | 9, 10 | bitri 275 |
. . . . . . . . 9
β’
(βπ β
π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β (π¦ = (π β¨ π) β§ (π β π β§ βπ β π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))))) |
12 | 11 | exbii 1851 |
. . . . . . . 8
β’
(βπ¦βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ¦(π¦ = (π β¨ π) β§ (π β π β§ βπ β π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))))) |
13 | | ovex 7395 |
. . . . . . . . 9
β’ (π β¨ π) β V |
14 | | an12 644 |
. . . . . . . . . . . 12
β’ ((π β π β§ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) β (π¦ β π΅ β§ (π β π β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
15 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β¨ π) β (π¦ β π΅ β (π β¨ π) β π΅)) |
16 | | breq2 5114 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (π β¨ π) β (π β€ π¦ β π β€ (π β¨ π))) |
17 | 16 | notbid 318 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (π β¨ π) β (Β¬ π β€ π¦ β Β¬ π β€ (π β¨ π))) |
18 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (π β¨ π) β (π¦ β¨ π) = ((π β¨ π) β¨ π)) |
19 | 18 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (π β¨ π) β (π = (π¦ β¨ π) β π = ((π β¨ π) β¨ π))) |
20 | 17, 19 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π β¨ π) β ((Β¬ π β€ π¦ β§ π = (π¦ β¨ π)) β (Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
21 | 20 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π β¨ π) β ((π β π β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β (π β π β§ (Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))))) |
22 | | 3anass 1096 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)) β (π β π β§ (Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
23 | 21, 22 | bitr4di 289 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β¨ π) β ((π β π β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
24 | 15, 23 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π¦ = (π β¨ π) β ((π¦ β π΅ β§ (π β π β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) β ((π β¨ π) β π΅ β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))))) |
25 | 14, 24 | bitrid 283 |
. . . . . . . . . . 11
β’ (π¦ = (π β¨ π) β ((π β π β§ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) β ((π β¨ π) β π΅ β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))))) |
26 | 25 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π¦ = (π β¨ π) β (βπ β π΄ (π β π β§ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) β βπ β π΄ ((π β¨ π) β π΅ β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))))) |
27 | | r19.42v 3188 |
. . . . . . . . . 10
β’
(βπ β
π΄ (π β π β§ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) β (π β π β§ βπ β π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
28 | | r19.42v 3188 |
. . . . . . . . . 10
β’
(βπ β
π΄ ((π β¨ π) β π΅ β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))) β ((π β¨ π) β π΅ β§ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
29 | 26, 27, 28 | 3bitr3g 313 |
. . . . . . . . 9
β’ (π¦ = (π β¨ π) β ((π β π β§ βπ β π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) β ((π β¨ π) β π΅ β§ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))))) |
30 | 13, 29 | ceqsexv 3497 |
. . . . . . . 8
β’
(βπ¦(π¦ = (π β¨ π) β§ (π β π β§ βπ β π΄ (π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) β ((π β¨ π) β π΅ β§ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
31 | 12, 30 | bitri 275 |
. . . . . . 7
β’
(βπ¦βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β ((π β¨ π) β π΅ β§ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
32 | | simpll 766 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄)) β πΎ β HL) |
33 | | simprl 770 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄)) β π β π΄) |
34 | | simprr 772 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄)) β π β π΄) |
35 | 1, 3, 4 | hlatjcl 37858 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β π΅) |
36 | 32, 33, 34, 35 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄)) β (π β¨ π) β π΅) |
37 | 36 | biantrurd 534 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄)) β (βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)) β ((π β¨ π) β π΅ β§ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))))) |
38 | 31, 37 | bitr4id 290 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄)) β (βπ¦βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
39 | 38 | 2rexbidva 3212 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (βπ β π΄ βπ β π΄ βπ¦βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
40 | | rexcom4 3274 |
. . . . . . 7
β’
(βπ β
π΄ βπ¦βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ¦βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
41 | 40 | rexbii 3098 |
. . . . . 6
β’
(βπ β
π΄ βπ β π΄ βπ¦βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ βπ¦βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
42 | | rexcom4 3274 |
. . . . . 6
β’
(βπ β
π΄ βπ¦βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ¦βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
43 | 41, 42 | bitri 275 |
. . . . 5
β’
(βπ β
π΄ βπ β π΄ βπ¦βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ¦βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
44 | 39, 43 | bitr3di 286 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)) β βπ¦βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))))) |
45 | | rexcom 3276 |
. . . . . . . . 9
β’
(βπ β
π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
46 | 45 | rexbii 3098 |
. . . . . . . 8
β’
(βπ β
π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
47 | | rexcom 3276 |
. . . . . . . 8
β’
(βπ β
π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
48 | 46, 47 | bitri 275 |
. . . . . . 7
β’
(βπ β
π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
49 | 1, 3, 4, 5 | islln2 38003 |
. . . . . . . . . . 11
β’ (πΎ β HL β (π¦ β (LLinesβπΎ) β (π¦ β π΅ β§ βπ β π΄ βπ β π΄ (π β π β§ π¦ = (π β¨ π))))) |
50 | 49 | adantr 482 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΅) β (π¦ β (LLinesβπΎ) β (π¦ β π΅ β§ βπ β π΄ βπ β π΄ (π β π β§ π¦ = (π β¨ π))))) |
51 | 50 | anbi1d 631 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΅) β ((π¦ β (LLinesβπΎ) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β ((π¦ β π΅ β§ βπ β π΄ βπ β π΄ (π β π β§ π¦ = (π β¨ π))) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
52 | | r19.42v 3188 |
. . . . . . . . . 10
β’
(βπ β
π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ βπ β π΄ (π β π β§ π¦ = (π β¨ π))) β ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ βπ β π΄ βπ β π΄ (π β π β§ π¦ = (π β¨ π)))) |
53 | | r19.42v 3188 |
. . . . . . . . . . 11
β’
(βπ β
π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ βπ β π΄ (π β π β§ π¦ = (π β¨ π)))) |
54 | 53 | rexbii 3098 |
. . . . . . . . . 10
β’
(βπ β
π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ βπ β π΄ (π β π β§ π¦ = (π β¨ π)))) |
55 | | an32 645 |
. . . . . . . . . 10
β’ (((π¦ β π΅ β§ βπ β π΄ βπ β π΄ (π β π β§ π¦ = (π β¨ π))) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ βπ β π΄ βπ β π΄ (π β π β§ π¦ = (π β¨ π)))) |
56 | 52, 54, 55 | 3bitr4ri 304 |
. . . . . . . . 9
β’ (((π¦ β π΅ β§ βπ β π΄ βπ β π΄ (π β π β§ π¦ = (π β¨ π))) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π)))) |
57 | 51, 56 | bitrdi 287 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΅) β ((π¦ β (LLinesβπΎ) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))))) |
58 | 57 | rexbidv 3176 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΅) β (βπ β π΄ (π¦ β (LLinesβπΎ) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))))) |
59 | 48, 58 | bitr4id 290 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅) β (βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ β π΄ (π¦ β (LLinesβπΎ) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
60 | | r19.42v 3188 |
. . . . . 6
β’
(βπ β
π΄ (π¦ β (LLinesβπΎ) β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β (π¦ β (LLinesβπΎ) β§ βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) |
61 | 59, 60 | bitrdi 287 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β (π¦ β (LLinesβπΎ) β§ βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
62 | 61 | exbidv 1925 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (βπ¦βπ β π΄ βπ β π΄ βπ β π΄ ((π¦ β π΅ β§ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) β§ (π β π β§ π¦ = (π β¨ π))) β βπ¦(π¦ β (LLinesβπΎ) β§ βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
63 | 44, 62 | bitrd 279 |
. . 3
β’ ((πΎ β HL β§ π β π΅) β (βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)) β βπ¦(π¦ β (LLinesβπΎ) β§ βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
64 | 8, 63 | bitr4id 290 |
. 2
β’ ((πΎ β HL β§ π β π΅) β (βπ¦ β (LLinesβπΎ)βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |
65 | 7, 64 | bitrd 279 |
1
β’ ((πΎ β HL β§ π β π΅) β (π β π β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) |