Step | Hyp | Ref
| Expression |
1 | | lshpdisj.w |
. . . . . . . . 9
β’ (π β π β LVec) |
2 | | lveclmod 20583 |
. . . . . . . . 9
β’ (π β LVec β π β LMod) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
β’ (π β π β LMod) |
4 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ π£ β π) β π β LMod) |
5 | | lshpdisj.x |
. . . . . . . 8
β’ (π β π β π) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π£ β π) β π β π) |
7 | | eqid 2737 |
. . . . . . . 8
β’
(Scalarβπ) =
(Scalarβπ) |
8 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
9 | | lshpdisj.v |
. . . . . . . 8
β’ π = (Baseβπ) |
10 | | eqid 2737 |
. . . . . . . 8
β’ (
Β·π βπ) = ( Β·π
βπ) |
11 | | lshpdisj.n |
. . . . . . . 8
β’ π = (LSpanβπ) |
12 | 7, 8, 9, 10, 11 | lspsnel 20480 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (π£ β (πβ{π}) β βπ β (Baseβ(Scalarβπ))π£ = (π( Β·π
βπ)π))) |
13 | 4, 6, 12 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π£ β π) β (π£ β (πβ{π}) β βπ β (Baseβ(Scalarβπ))π£ = (π( Β·π
βπ)π))) |
14 | | lshpdisj.p |
. . . . . . . . . . . . . . . . 17
β’ β =
(LSSumβπ) |
15 | | lshpdisj.h |
. . . . . . . . . . . . . . . . 17
β’ π» = (LSHypβπ) |
16 | | lshpdisj.u |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π») |
17 | | lshpdisj.e |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (πβ{π})) = π) |
18 | 9, 11, 14, 15, 3, 16, 5, 17 | lshpnel 37474 |
. . . . . . . . . . . . . . . 16
β’ (π β Β¬ π β π) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β Β¬ π β π) |
20 | | lshpdisj.o |
. . . . . . . . . . . . . . . 16
β’ 0 =
(0gβπ) |
21 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(LSubSpβπ) =
(LSubSpβπ) |
22 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β π β LVec) |
23 | 21, 15, 3, 16 | lshplss 37472 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (LSubSpβπ)) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β π β (LSubSpβπ)) |
25 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β π β π) |
26 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (Baseβ(Scalarβπ))) β π β LMod) |
27 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (Baseβ(Scalarβπ))) β π β (Baseβ(Scalarβπ))) |
28 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (Baseβ(Scalarβπ))) β π β π) |
29 | 9, 10, 7, 8, 11, 26, 27, 28 | lspsneli 20478 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (Baseβ(Scalarβπ))) β (π( Β·π
βπ)π) β (πβ{π})) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β (π(
Β·π βπ)π) β (πβ{π})) |
31 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β (π(
Β·π βπ)π) β 0 ) |
32 | 9, 20, 21, 11, 22, 24, 25, 30, 31 | lspsnel4 20601 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β (π β π β (π( Β·π
βπ)π) β π)) |
33 | 19, 32 | mtbid 324 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (Baseβ(Scalarβπ))) β§ (π( Β·π
βπ)π) β 0 ) β Β¬ (π(
Β·π βπ)π) β π) |
34 | 33 | ex 414 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (Baseβ(Scalarβπ))) β ((π( Β·π
βπ)π) β 0 β Β¬ (π(
Β·π βπ)π) β π)) |
35 | 34 | necon4ad 2963 |
. . . . . . . . . . . 12
β’ ((π β§ π β (Baseβ(Scalarβπ))) β ((π( Β·π
βπ)π) β π β (π( Β·π
βπ)π) = 0 )) |
36 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (π£ = (π( Β·π
βπ)π) β (π£ β π β (π( Β·π
βπ)π) β π)) |
37 | | eqeq1 2741 |
. . . . . . . . . . . . 13
β’ (π£ = (π( Β·π
βπ)π) β (π£ = 0 β (π( Β·π
βπ)π) = 0 )) |
38 | 36, 37 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π£ = (π( Β·π
βπ)π) β ((π£ β π β π£ = 0 ) β ((π(
Β·π βπ)π) β π β (π( Β·π
βπ)π) = 0 ))) |
39 | 35, 38 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((π β§ π β (Baseβ(Scalarβπ))) β (π£ = (π( Β·π
βπ)π) β (π£ β π β π£ = 0 ))) |
40 | 39 | ex 414 |
. . . . . . . . . 10
β’ (π β (π β (Baseβ(Scalarβπ)) β (π£ = (π( Β·π
βπ)π) β (π£ β π β π£ = 0 )))) |
41 | 40 | com23 86 |
. . . . . . . . 9
β’ (π β (π£ = (π( Β·π
βπ)π) β (π β (Baseβ(Scalarβπ)) β (π£ β π β π£ = 0 )))) |
42 | 41 | com24 95 |
. . . . . . . 8
β’ (π β (π£ β π β (π β (Baseβ(Scalarβπ)) β (π£ = (π( Β·π
βπ)π) β π£ = 0 )))) |
43 | 42 | imp31 419 |
. . . . . . 7
β’ (((π β§ π£ β π) β§ π β (Baseβ(Scalarβπ))) β (π£ = (π( Β·π
βπ)π) β π£ = 0 )) |
44 | 43 | rexlimdva 3153 |
. . . . . 6
β’ ((π β§ π£ β π) β (βπ β (Baseβ(Scalarβπ))π£ = (π( Β·π
βπ)π) β π£ = 0 )) |
45 | 13, 44 | sylbid 239 |
. . . . 5
β’ ((π β§ π£ β π) β (π£ β (πβ{π}) β π£ = 0 )) |
46 | 45 | expimpd 455 |
. . . 4
β’ (π β ((π£ β π β§ π£ β (πβ{π})) β π£ = 0 )) |
47 | | elin 3931 |
. . . 4
β’ (π£ β (π β© (πβ{π})) β (π£ β π β§ π£ β (πβ{π}))) |
48 | | velsn 4607 |
. . . 4
β’ (π£ β { 0 } β π£ = 0 ) |
49 | 46, 47, 48 | 3imtr4g 296 |
. . 3
β’ (π β (π£ β (π β© (πβ{π})) β π£ β { 0 })) |
50 | 49 | ssrdv 3955 |
. 2
β’ (π β (π β© (πβ{π})) β { 0 }) |
51 | 9, 21, 11 | lspsncl 20454 |
. . . . 5
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
52 | 3, 5, 51 | syl2anc 585 |
. . . 4
β’ (π β (πβ{π}) β (LSubSpβπ)) |
53 | 21 | lssincl 20442 |
. . . 4
β’ ((π β LMod β§ π β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β (π β© (πβ{π})) β (LSubSpβπ)) |
54 | 3, 23, 52, 53 | syl3anc 1372 |
. . 3
β’ (π β (π β© (πβ{π})) β (LSubSpβπ)) |
55 | 20, 21 | lss0ss 20425 |
. . 3
β’ ((π β LMod β§ (π β© (πβ{π})) β (LSubSpβπ)) β { 0 } β (π β© (πβ{π}))) |
56 | 3, 54, 55 | syl2anc 585 |
. 2
β’ (π β { 0 } β (π β© (πβ{π}))) |
57 | 50, 56 | eqssd 3966 |
1
β’ (π β (π β© (πβ{π})) = { 0 }) |