Step | Hyp | Ref
| Expression |
1 | | dvh3dim.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | dvh3dim.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
3 | | dvh3dim.v |
. . . . 5
β’ π = (Baseβπ) |
4 | | dvh3dim.n |
. . . . 5
β’ π = (LSpanβπ) |
5 | | dvh3dim.k |
. . . . 5
β’ (π β (πΎ β HL β§ π β π»)) |
6 | | dvh3dim.x |
. . . . 5
β’ (π β π β π) |
7 | | dvh3dim2.z |
. . . . 5
β’ (π β π β π) |
8 | 1, 2, 3, 4, 5, 6, 7 | dvh3dim 39955 |
. . . 4
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π})) |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ π β (πβ{π, π})) β βπ§ β π Β¬ π§ β (πβ{π, π})) |
10 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
11 | 1, 2, 5 | dvhlmod 39619 |
. . . . . . . 8
β’ (π β π β LMod) |
12 | 11 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (πβ{π, π})) β§ π§ β π) β π β LMod) |
13 | 3, 10, 4, 11, 6, 7 | lspprcl 20454 |
. . . . . . . 8
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
14 | 13 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (πβ{π, π})) β§ π§ β π) β (πβ{π, π}) β (LSubSpβπ)) |
15 | 3, 4, 11, 6, 7 | lspprid1 20473 |
. . . . . . . 8
β’ (π β π β (πβ{π, π})) |
16 | 15 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (πβ{π, π})) β§ π§ β π) β π β (πβ{π, π})) |
17 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β (πβ{π, π})) β§ π§ β π) β π β (πβ{π, π})) |
18 | 10, 4, 12, 14, 16, 17 | lspprss 20468 |
. . . . . 6
β’ (((π β§ π β (πβ{π, π})) β§ π§ β π) β (πβ{π, π}) β (πβ{π, π})) |
19 | 18 | ssneld 3947 |
. . . . 5
β’ (((π β§ π β (πβ{π, π})) β§ π§ β π) β (Β¬ π§ β (πβ{π, π}) β Β¬ π§ β (πβ{π, π}))) |
20 | 19 | ancrd 553 |
. . . 4
β’ (((π β§ π β (πβ{π, π})) β§ π§ β π) β (Β¬ π§ β (πβ{π, π}) β (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π})))) |
21 | 20 | reximdva 3162 |
. . 3
β’ ((π β§ π β (πβ{π, π})) β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π})))) |
22 | 9, 21 | mpd 15 |
. 2
β’ ((π β§ π β (πβ{π, π})) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |
23 | | dvh3dim.y |
. . . . 5
β’ (π β π β π) |
24 | 1, 2, 3, 4, 5, 6, 23 | dvh3dim 39955 |
. . . 4
β’ (π β βπ€ β π Β¬ π€ β (πβ{π, π})) |
25 | 24 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β βπ€ β π Β¬ π€ β (πβ{π, π})) |
26 | | simpl1l 1225 |
. . . . . . . 8
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β π) |
27 | 26, 11 | syl 17 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β π β LMod) |
28 | | simpl2 1193 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β π€ β π) |
29 | 26, 23 | syl 17 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β π β π) |
30 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ) = (+gβπ) |
31 | 3, 30 | lmodvacl 20351 |
. . . . . . 7
β’ ((π β LMod β§ π€ β π β§ π β π) β (π€(+gβπ)π) β π) |
32 | 27, 28, 29, 31 | syl3anc 1372 |
. . . . . 6
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β (π€(+gβπ)π) β π) |
33 | 3, 10, 4, 11, 6, 23 | lspprcl 20454 |
. . . . . . . 8
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
34 | 26, 33 | syl 17 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β (πβ{π, π}) β (LSubSpβπ)) |
35 | 3, 4, 11, 6, 23 | lspprid2 20474 |
. . . . . . . 8
β’ (π β π β (πβ{π, π})) |
36 | 26, 35 | syl 17 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β π β (πβ{π, π})) |
37 | | simpl3 1194 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β Β¬ π€ β (πβ{π, π})) |
38 | 3, 30, 10, 27, 34, 36, 28, 37 | lssvancl2 20421 |
. . . . . 6
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β Β¬ (π€(+gβπ)π) β (πβ{π, π})) |
39 | 26, 13 | syl 17 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β (πβ{π, π}) β (LSubSpβπ)) |
40 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β π€ β (πβ{π, π})) |
41 | | simpl1r 1226 |
. . . . . . 7
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β Β¬ π β (πβ{π, π})) |
42 | 3, 30, 10, 27, 39, 40, 29, 41 | lssvancl1 20420 |
. . . . . 6
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β Β¬ (π€(+gβπ)π) β (πβ{π, π})) |
43 | | eleq1 2822 |
. . . . . . . . 9
β’ (π§ = (π€(+gβπ)π) β (π§ β (πβ{π, π}) β (π€(+gβπ)π) β (πβ{π, π}))) |
44 | 43 | notbid 318 |
. . . . . . . 8
β’ (π§ = (π€(+gβπ)π) β (Β¬ π§ β (πβ{π, π}) β Β¬ (π€(+gβπ)π) β (πβ{π, π}))) |
45 | | eleq1 2822 |
. . . . . . . . 9
β’ (π§ = (π€(+gβπ)π) β (π§ β (πβ{π, π}) β (π€(+gβπ)π) β (πβ{π, π}))) |
46 | 45 | notbid 318 |
. . . . . . . 8
β’ (π§ = (π€(+gβπ)π) β (Β¬ π§ β (πβ{π, π}) β Β¬ (π€(+gβπ)π) β (πβ{π, π}))) |
47 | 44, 46 | anbi12d 632 |
. . . . . . 7
β’ (π§ = (π€(+gβπ)π) β ((Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π})) β (Β¬ (π€(+gβπ)π) β (πβ{π, π}) β§ Β¬ (π€(+gβπ)π) β (πβ{π, π})))) |
48 | 47 | rspcev 3580 |
. . . . . 6
β’ (((π€(+gβπ)π) β π β§ (Β¬ (π€(+gβπ)π) β (πβ{π, π}) β§ Β¬ (π€(+gβπ)π) β (πβ{π, π}))) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |
49 | 32, 38, 42, 48 | syl12anc 836 |
. . . . 5
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ π€ β (πβ{π, π})) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |
50 | | simpl2 1193 |
. . . . . 6
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ Β¬ π€ β (πβ{π, π})) β π€ β π) |
51 | | simpl3 1194 |
. . . . . 6
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ Β¬ π€ β (πβ{π, π})) β Β¬ π€ β (πβ{π, π})) |
52 | | simpr 486 |
. . . . . 6
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ Β¬ π€ β (πβ{π, π})) β Β¬ π€ β (πβ{π, π})) |
53 | | eleq1 2822 |
. . . . . . . . 9
β’ (π§ = π€ β (π§ β (πβ{π, π}) β π€ β (πβ{π, π}))) |
54 | 53 | notbid 318 |
. . . . . . . 8
β’ (π§ = π€ β (Β¬ π§ β (πβ{π, π}) β Β¬ π€ β (πβ{π, π}))) |
55 | | eleq1 2822 |
. . . . . . . . 9
β’ (π§ = π€ β (π§ β (πβ{π, π}) β π€ β (πβ{π, π}))) |
56 | 55 | notbid 318 |
. . . . . . . 8
β’ (π§ = π€ β (Β¬ π§ β (πβ{π, π}) β Β¬ π€ β (πβ{π, π}))) |
57 | 54, 56 | anbi12d 632 |
. . . . . . 7
β’ (π§ = π€ β ((Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π})) β (Β¬ π€ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π})))) |
58 | 57 | rspcev 3580 |
. . . . . 6
β’ ((π€ β π β§ (Β¬ π€ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |
59 | 50, 51, 52, 58 | syl12anc 836 |
. . . . 5
β’ ((((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β§ Β¬ π€ β (πβ{π, π})) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |
60 | 49, 59 | pm2.61dan 812 |
. . . 4
β’ (((π β§ Β¬ π β (πβ{π, π})) β§ π€ β π β§ Β¬ π€ β (πβ{π, π})) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |
61 | 60 | rexlimdv3a 3153 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β (βπ€ β π Β¬ π€ β (πβ{π, π}) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π})))) |
62 | 25, 61 | mpd 15 |
. 2
β’ ((π β§ Β¬ π β (πβ{π, π})) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |
63 | 22, 62 | pm2.61dan 812 |
1
β’ (π β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{π, π}))) |