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.y |
. . . . 5
β’ (π β π β π) |
7 | | dvh3dim2.z |
. . . . 5
β’ (π β π β π) |
8 | 1, 2, 3, 4, 5, 6, 7 | dvh3dim 40317 |
. . . 4
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π})) |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ π = (0gβπ)) β βπ§ β π Β¬ π§ β (πβ{π, π})) |
10 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
11 | 1, 2, 5 | dvhlmod 39981 |
. . . . . . . 8
β’ (π β π β LMod) |
12 | | prssi 4825 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β {π, π} β π) |
13 | 6, 7, 12 | syl2anc 585 |
. . . . . . . 8
β’ (π β {π, π} β π) |
14 | 3, 10, 4, 11, 13 | lspun0 20622 |
. . . . . . 7
β’ (π β (πβ({π, π} βͺ {(0gβπ)})) = (πβ{π, π})) |
15 | | tprot 4754 |
. . . . . . . . . 10
β’
{(0gβπ), π, π} = {π, π, (0gβπ)} |
16 | | df-tp 4634 |
. . . . . . . . . 10
β’ {π, π, (0gβπ)} = ({π, π} βͺ {(0gβπ)}) |
17 | 15, 16 | eqtr2i 2762 |
. . . . . . . . 9
β’ ({π, π} βͺ {(0gβπ)}) =
{(0gβπ),
π, π} |
18 | | tpeq1 4747 |
. . . . . . . . 9
β’ (π = (0gβπ) β {π, π, π} = {(0gβπ), π, π}) |
19 | 17, 18 | eqtr4id 2792 |
. . . . . . . 8
β’ (π = (0gβπ) β ({π, π} βͺ {(0gβπ)}) = {π, π, π}) |
20 | 19 | fveq2d 6896 |
. . . . . . 7
β’ (π = (0gβπ) β (πβ({π, π} βͺ {(0gβπ)})) = (πβ{π, π, π})) |
21 | 14, 20 | sylan9req 2794 |
. . . . . 6
β’ ((π β§ π = (0gβπ)) β (πβ{π, π}) = (πβ{π, π, π})) |
22 | 21 | eleq2d 2820 |
. . . . 5
β’ ((π β§ π = (0gβπ)) β (π§ β (πβ{π, π}) β π§ β (πβ{π, π, π}))) |
23 | 22 | notbid 318 |
. . . 4
β’ ((π β§ π = (0gβπ)) β (Β¬ π§ β (πβ{π, π}) β Β¬ π§ β (πβ{π, π, π}))) |
24 | 23 | rexbidv 3179 |
. . 3
β’ ((π β§ π = (0gβπ)) β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π Β¬ π§ β (πβ{π, π, π}))) |
25 | 9, 24 | mpbid 231 |
. 2
β’ ((π β§ π = (0gβπ)) β βπ§ β π Β¬ π§ β (πβ{π, π, π})) |
26 | | dvh3dim.x |
. . . . 5
β’ (π β π β π) |
27 | 1, 2, 3, 4, 5, 26,
7 | dvh3dim 40317 |
. . . 4
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π})) |
28 | 27 | adantr 482 |
. . 3
β’ ((π β§ π = (0gβπ)) β βπ§ β π Β¬ π§ β (πβ{π, π})) |
29 | | prssi 4825 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β {π, π} β π) |
30 | 26, 7, 29 | syl2anc 585 |
. . . . . . . 8
β’ (π β {π, π} β π) |
31 | 3, 10, 4, 11, 30 | lspun0 20622 |
. . . . . . 7
β’ (π β (πβ({π, π} βͺ {(0gβπ)})) = (πβ{π, π})) |
32 | | df-tp 4634 |
. . . . . . . . . 10
β’ {π, π, (0gβπ)} = ({π, π} βͺ {(0gβπ)}) |
33 | | tpcomb 4756 |
. . . . . . . . . 10
β’ {π, π, (0gβπ)} = {π, (0gβπ), π} |
34 | 32, 33 | eqtr3i 2763 |
. . . . . . . . 9
β’ ({π, π} βͺ {(0gβπ)}) = {π, (0gβπ), π} |
35 | | tpeq2 4748 |
. . . . . . . . 9
β’ (π = (0gβπ) β {π, π, π} = {π, (0gβπ), π}) |
36 | 34, 35 | eqtr4id 2792 |
. . . . . . . 8
β’ (π = (0gβπ) β ({π, π} βͺ {(0gβπ)}) = {π, π, π}) |
37 | 36 | fveq2d 6896 |
. . . . . . 7
β’ (π = (0gβπ) β (πβ({π, π} βͺ {(0gβπ)})) = (πβ{π, π, π})) |
38 | 31, 37 | sylan9req 2794 |
. . . . . 6
β’ ((π β§ π = (0gβπ)) β (πβ{π, π}) = (πβ{π, π, π})) |
39 | 38 | eleq2d 2820 |
. . . . 5
β’ ((π β§ π = (0gβπ)) β (π§ β (πβ{π, π}) β π§ β (πβ{π, π, π}))) |
40 | 39 | notbid 318 |
. . . 4
β’ ((π β§ π = (0gβπ)) β (Β¬ π§ β (πβ{π, π}) β Β¬ π§ β (πβ{π, π, π}))) |
41 | 40 | rexbidv 3179 |
. . 3
β’ ((π β§ π = (0gβπ)) β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π Β¬ π§ β (πβ{π, π, π}))) |
42 | 28, 41 | mpbid 231 |
. 2
β’ ((π β§ π = (0gβπ)) β βπ§ β π Β¬ π§ β (πβ{π, π, π})) |
43 | 1, 2, 3, 4, 5, 26,
6 | dvh3dim 40317 |
. . . 4
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π})) |
44 | 43 | adantr 482 |
. . 3
β’ ((π β§ π = (0gβπ)) β βπ§ β π Β¬ π§ β (πβ{π, π})) |
45 | | prssi 4825 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β {π, π} β π) |
46 | 26, 6, 45 | syl2anc 585 |
. . . . . . . 8
β’ (π β {π, π} β π) |
47 | 3, 10, 4, 11, 46 | lspun0 20622 |
. . . . . . 7
β’ (π β (πβ({π, π} βͺ {(0gβπ)})) = (πβ{π, π})) |
48 | | tpeq3 4749 |
. . . . . . . . 9
β’ (π = (0gβπ) β {π, π, π} = {π, π, (0gβπ)}) |
49 | | df-tp 4634 |
. . . . . . . . 9
β’ {π, π, (0gβπ)} = ({π, π} βͺ {(0gβπ)}) |
50 | 48, 49 | eqtr2di 2790 |
. . . . . . . 8
β’ (π = (0gβπ) β ({π, π} βͺ {(0gβπ)}) = {π, π, π}) |
51 | 50 | fveq2d 6896 |
. . . . . . 7
β’ (π = (0gβπ) β (πβ({π, π} βͺ {(0gβπ)})) = (πβ{π, π, π})) |
52 | 47, 51 | sylan9req 2794 |
. . . . . 6
β’ ((π β§ π = (0gβπ)) β (πβ{π, π}) = (πβ{π, π, π})) |
53 | 52 | eleq2d 2820 |
. . . . 5
β’ ((π β§ π = (0gβπ)) β (π§ β (πβ{π, π}) β π§ β (πβ{π, π, π}))) |
54 | 53 | notbid 318 |
. . . 4
β’ ((π β§ π = (0gβπ)) β (Β¬ π§ β (πβ{π, π}) β Β¬ π§ β (πβ{π, π, π}))) |
55 | 54 | rexbidv 3179 |
. . 3
β’ ((π β§ π = (0gβπ)) β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π Β¬ π§ β (πβ{π, π, π}))) |
56 | 44, 55 | mpbid 231 |
. 2
β’ ((π β§ π = (0gβπ)) β βπ§ β π Β¬ π§ β (πβ{π, π, π})) |
57 | 5 | adantr 482 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β (πΎ β HL β§ π β π»)) |
58 | 26 | adantr 482 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β π β π) |
59 | 6 | adantr 482 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β π β π) |
60 | 7 | adantr 482 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β π β π) |
61 | | simpr1 1195 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β π β (0gβπ)) |
62 | | simpr2 1196 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β π β (0gβπ)) |
63 | | simpr3 1197 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β π β (0gβπ)) |
64 | 1, 2, 3, 4, 57, 58, 59, 60, 10, 61, 62, 63 | dvh4dimlem 40314 |
. 2
β’ ((π β§ (π β (0gβπ) β§ π β (0gβπ) β§ π β (0gβπ))) β βπ§ β π Β¬ π§ β (πβ{π, π, π})) |
65 | 25, 42, 56, 64 | pm2.61da3ne 3032 |
1
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π, π})) |