Step | Hyp | Ref
| Expression |
1 | | mapdh8a.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
2 | | mapdh8a.u |
. . . . . . 7
β’ π = ((DVecHβπΎ)βπ) |
3 | | mapdh8a.v |
. . . . . . 7
β’ π = (Baseβπ) |
4 | | mapdh8a.s |
. . . . . . 7
β’ β =
(-gβπ) |
5 | | mapdh8a.o |
. . . . . . 7
β’ 0 =
(0gβπ) |
6 | | mapdh8a.n |
. . . . . . 7
β’ π = (LSpanβπ) |
7 | | mapdh8a.c |
. . . . . . 7
β’ πΆ = ((LCDualβπΎ)βπ) |
8 | | mapdh8a.d |
. . . . . . 7
β’ π· = (BaseβπΆ) |
9 | | mapdh8a.r |
. . . . . . 7
β’ π
= (-gβπΆ) |
10 | | mapdh8a.q |
. . . . . . 7
β’ π = (0gβπΆ) |
11 | | mapdh8a.j |
. . . . . . 7
β’ π½ = (LSpanβπΆ) |
12 | | mapdh8a.m |
. . . . . . 7
β’ π = ((mapdβπΎ)βπ) |
13 | | mapdh8a.i |
. . . . . . 7
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
14 | | mapdh8a.k |
. . . . . . . 8
β’ (π β (πΎ β HL β§ π β π»)) |
15 | 14 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πΎ β HL β§ π β π»)) |
16 | | mapdh8h.f |
. . . . . . . 8
β’ (π β πΉ β π·) |
17 | 16 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β πΉ β π·) |
18 | | mapdh8h.mn |
. . . . . . . 8
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
19 | 18 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πβ(πβ{π})) = (π½β{πΉ})) |
20 | | mapdh9a.x |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
21 | 20 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β π β (π β { 0 })) |
22 | | simp3ll 1245 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β π§ β (π β { 0 })) |
23 | | simp3rl 1247 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β π€ β (π β { 0 })) |
24 | | simplrl 776 |
. . . . . . . . 9
β’ (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πβ{π§}) β (πβ{π})) |
25 | 24 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πβ{π§}) β (πβ{π})) |
26 | 25 | necomd 2996 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πβ{π}) β (πβ{π§})) |
27 | | simprrl 780 |
. . . . . . . . 9
β’ (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πβ{π€}) β (πβ{π})) |
28 | 27 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πβ{π€}) β (πβ{π})) |
29 | 28 | necomd 2996 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πβ{π}) β (πβ{π€})) |
30 | | simplrr 777 |
. . . . . . . 8
β’ (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πβ{π§}) β (πβ{π})) |
31 | 30 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πβ{π§}) β (πβ{π})) |
32 | | simprrr 781 |
. . . . . . . 8
β’ (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πβ{π€}) β (πβ{π})) |
33 | 32 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πβ{π€}) β (πβ{π})) |
34 | | mapdh9a.t |
. . . . . . . 8
β’ (π β π β π) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β π β π) |
36 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 15, 17, 19, 21, 22, 23, 26, 29, 31, 33, 35 | mapdh8 40297 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) |
37 | 36 | 3exp 1120 |
. . . . 5
β’ (π β ((π§ β π β§ π€ β π) β (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)))) |
38 | 37 | ralrimivv 3192 |
. . . 4
β’ (π β βπ§ β π βπ€ β π (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©))) |
39 | 20 | eldifad 3923 |
. . . . . . . 8
β’ (π β π β π) |
40 | 1, 2, 3, 6, 14, 39, 34 | dvh3dim 39955 |
. . . . . . 7
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π})) |
41 | | eqid 2733 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
42 | 1, 2, 14 | dvhlmod 39619 |
. . . . . . . . . . . 12
β’ (π β π β LMod) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β LMod) |
44 | 3, 41, 6, 42, 39, 34 | lspprcl 20454 |
. . . . . . . . . . . 12
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π, π}) β (LSubSpβπ)) |
46 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π§ β π) |
47 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β Β¬ π§ β (πβ{π, π})) |
48 | 5, 41, 43, 45, 46, 47 | lssneln0 20428 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π§ β (π β { 0 })) |
49 | 1, 2, 14 | dvhlvec 39618 |
. . . . . . . . . . . 12
β’ (π β π β LVec) |
50 | 49 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β LVec) |
51 | 39 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β π) |
52 | 34 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β π) |
53 | 3, 6, 50, 46, 51, 52, 47 | lspindpi 20609 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) |
54 | 48, 53 | jca 513 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) |
55 | 54 | ex 414 |
. . . . . . . 8
β’ ((π β§ π§ β π) β (Β¬ π§ β (πβ{π, π}) β (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))))) |
56 | 55 | reximdva 3162 |
. . . . . . 7
β’ (π β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))))) |
57 | 40, 56 | mpd 15 |
. . . . . 6
β’ (π β βπ§ β π (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) |
58 | 14 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πΎ β HL β§ π β π»)) |
59 | 16 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β πΉ β π·) |
60 | 18 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πβ(πβ{π})) = (π½β{πΉ})) |
61 | 20 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β π β (π β { 0 })) |
62 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β π§ β π) |
63 | | simprrl 780 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πβ{π§}) β (πβ{π})) |
64 | 63 | necomd 2996 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πβ{π}) β (πβ{π§})) |
65 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 58, 59, 60, 61, 62, 64 | mapdhcl 40236 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πΌββ¨π, πΉ, π§β©) β π·) |
66 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πΌββ¨π, πΉ, π§β©) = (πΌββ¨π, πΉ, π§β©)) |
67 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β π§ β (π β { 0 })) |
68 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 58, 59, 60, 61, 67, 65, 64 | mapdheq 40237 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β ((πΌββ¨π, πΉ, π§β©) = (πΌββ¨π, πΉ, π§β©) β ((πβ(πβ{π§})) = (π½β{(πΌββ¨π, πΉ, π§β©)}) β§ (πβ(πβ{(π β π§)})) = (π½β{(πΉπ
(πΌββ¨π, πΉ, π§β©))})))) |
69 | 66, 68 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β ((πβ(πβ{π§})) = (π½β{(πΌββ¨π, πΉ, π§β©)}) β§ (πβ(πβ{(π β π§)})) = (π½β{(πΉπ
(πΌββ¨π, πΉ, π§β©))}))) |
70 | 69 | simpld 496 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πβ(πβ{π§})) = (π½β{(πΌββ¨π, πΉ, π§β©)})) |
71 | 34 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β π β π) |
72 | | simprrr 781 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πβ{π§}) β (πβ{π})) |
73 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 58, 65, 70, 67, 71, 72 | mapdhcl 40236 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·) |
74 | 73 | ex 414 |
. . . . . . . 8
β’ ((π β§ π§ β π) β ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·)) |
75 | 74 | ancld 552 |
. . . . . . 7
β’ ((π β§ π§ β π) β ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·))) |
76 | 75 | reximdva 3162 |
. . . . . 6
β’ (π β (βπ§ β π (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β βπ§ β π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·))) |
77 | 57, 76 | mpd 15 |
. . . . 5
β’ (π β βπ§ β π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·)) |
78 | | eleq1w 2817 |
. . . . . . 7
β’ (π§ = π€ β (π§ β (π β { 0 }) β π€ β (π β { 0 }))) |
79 | | sneq 4597 |
. . . . . . . . . 10
β’ (π§ = π€ β {π§} = {π€}) |
80 | 79 | fveq2d 6847 |
. . . . . . . . 9
β’ (π§ = π€ β (πβ{π§}) = (πβ{π€})) |
81 | 80 | neeq1d 3000 |
. . . . . . . 8
β’ (π§ = π€ β ((πβ{π§}) β (πβ{π}) β (πβ{π€}) β (πβ{π}))) |
82 | 80 | neeq1d 3000 |
. . . . . . . 8
β’ (π§ = π€ β ((πβ{π§}) β (πβ{π}) β (πβ{π€}) β (πβ{π}))) |
83 | 81, 82 | anbi12d 632 |
. . . . . . 7
β’ (π§ = π€ β (((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})) β ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) |
84 | 78, 83 | anbi12d 632 |
. . . . . 6
β’ (π§ = π€ β ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))))) |
85 | | oteq1 4840 |
. . . . . . . 8
β’ (π§ = π€ β β¨π§, (πΌββ¨π, πΉ, π§β©), πβ© = β¨π€, (πΌββ¨π, πΉ, π§β©), πβ©) |
86 | | oteq3 4842 |
. . . . . . . . . 10
β’ (π§ = π€ β β¨π, πΉ, π§β© = β¨π, πΉ, π€β©) |
87 | 86 | fveq2d 6847 |
. . . . . . . . 9
β’ (π§ = π€ β (πΌββ¨π, πΉ, π§β©) = (πΌββ¨π, πΉ, π€β©)) |
88 | 87 | oteq2d 4844 |
. . . . . . . 8
β’ (π§ = π€ β β¨π€, (πΌββ¨π, πΉ, π§β©), πβ© = β¨π€, (πΌββ¨π, πΉ, π€β©), πβ©) |
89 | 85, 88 | eqtrd 2773 |
. . . . . . 7
β’ (π§ = π€ β β¨π§, (πΌββ¨π, πΉ, π§β©), πβ© = β¨π€, (πΌββ¨π, πΉ, π€β©), πβ©) |
90 | 89 | fveq2d 6847 |
. . . . . 6
β’ (π§ = π€ β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) |
91 | 84, 90 | reusv3 5361 |
. . . . 5
β’
(βπ§ β
π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·) β (βπ§ β π βπ€ β π (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) β βπ¦ β π· βπ§ β π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
92 | 77, 91 | syl 17 |
. . . 4
β’ (π β (βπ§ β π βπ€ β π (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β§ (π€ β (π β { 0 }) β§ ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π})))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) β βπ¦ β π· βπ§ β π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
93 | 38, 92 | mpbid 231 |
. . 3
β’ (π β βπ¦ β π· βπ§ β π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) |
94 | | ioran 983 |
. . . . . . . 8
β’ (Β¬
(π§ β (πβ{π}) β¨ π§ β (πβ{π})) β (Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π}))) |
95 | | elun 4109 |
. . . . . . . 8
β’ (π§ β ((πβ{π}) βͺ (πβ{π})) β (π§ β (πβ{π}) β¨ π§ β (πβ{π}))) |
96 | 94, 95 | xchnxbir 333 |
. . . . . . 7
β’ (Β¬
π§ β ((πβ{π}) βͺ (πβ{π})) β (Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π}))) |
97 | 42 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π}))) β π β LMod) |
98 | 3, 41, 6 | lspsncl 20453 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
99 | 42, 39, 98 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (LSubSpβπ)) |
100 | 99 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π}))) β (πβ{π}) β (LSubSpβπ)) |
101 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π}))) β π§ β π) |
102 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π}))) β Β¬ π§ β (πβ{π})) |
103 | 5, 41, 97, 100, 101, 102 | lssneln0 20428 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π}))) β π§ β (π β { 0 })) |
104 | 103 | ex 414 |
. . . . . . . 8
β’ ((π β§ π§ β π) β ((Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π})) β π§ β (π β { 0 }))) |
105 | 42 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β π β LMod) |
106 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β π§ β π) |
107 | 39 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β π β π) |
108 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β Β¬ π§ β (πβ{π})) |
109 | 3, 6, 105, 106, 107, 108 | lspsnne2 20595 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β (πβ{π§}) β (πβ{π})) |
110 | 109 | ex 414 |
. . . . . . . . 9
β’ ((π β§ π§ β π) β (Β¬ π§ β (πβ{π}) β (πβ{π§}) β (πβ{π}))) |
111 | 42 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β π β LMod) |
112 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β π§ β π) |
113 | 34 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β π β π) |
114 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β Β¬ π§ β (πβ{π})) |
115 | 3, 6, 111, 112, 113, 114 | lspsnne2 20595 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π})) β (πβ{π§}) β (πβ{π})) |
116 | 115 | ex 414 |
. . . . . . . . 9
β’ ((π β§ π§ β π) β (Β¬ π§ β (πβ{π}) β (πβ{π§}) β (πβ{π}))) |
117 | 110, 116 | anim12d 610 |
. . . . . . . 8
β’ ((π β§ π§ β π) β ((Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π})) β ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π})))) |
118 | 104, 117 | jcad 514 |
. . . . . . 7
β’ ((π β§ π§ β π) β ((Β¬ π§ β (πβ{π}) β§ Β¬ π§ β (πβ{π})) β (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))))) |
119 | 96, 118 | biimtrid 241 |
. . . . . 6
β’ ((π β§ π§ β π) β (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β (π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))))) |
120 | 119 | imim1d 82 |
. . . . 5
β’ ((π β§ π§ β π) β (((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
121 | 120 | ralimdva 3161 |
. . . 4
β’ (π β (βπ§ β π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
122 | 121 | reximdv 3164 |
. . 3
β’ (π β (βπ¦ β π· βπ§ β π ((π§ β (π β { 0 }) β§ ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β βπ¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
123 | 93, 122 | mpd 15 |
. 2
β’ (π β βπ¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) |
124 | 3, 6, 42, 39, 34 | lspprid1 20473 |
. . . . . . . 8
β’ (π β π β (πβ{π, π})) |
125 | 41, 6, 42, 44, 124 | lspsnel5a 20472 |
. . . . . . 7
β’ (π β (πβ{π}) β (πβ{π, π})) |
126 | 3, 6, 42, 39, 34 | lspprid2 20474 |
. . . . . . . 8
β’ (π β π β (πβ{π, π})) |
127 | 41, 6, 42, 44, 126 | lspsnel5a 20472 |
. . . . . . 7
β’ (π β (πβ{π}) β (πβ{π, π})) |
128 | 125, 127 | unssd 4147 |
. . . . . 6
β’ (π β ((πβ{π}) βͺ (πβ{π})) β (πβ{π, π})) |
129 | 128 | ssneld 3947 |
. . . . 5
β’ (π β (Β¬ π§ β (πβ{π, π}) β Β¬ π§ β ((πβ{π}) βͺ (πβ{π})))) |
130 | 129 | reximdv 3164 |
. . . 4
β’ (π β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π Β¬ π§ β ((πβ{π}) βͺ (πβ{π})))) |
131 | 40, 130 | mpd 15 |
. . 3
β’ (π β βπ§ β π Β¬ π§ β ((πβ{π}) βͺ (πβ{π}))) |
132 | | reusv1 5353 |
. . 3
β’
(βπ§ β
π Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β (β!π¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β βπ¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
133 | 131, 132 | syl 17 |
. 2
β’ (π β (β!π¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β βπ¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
134 | 123, 133 | mpbird 257 |
1
β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) |