Step | Hyp | Ref
| Expression |
1 | | obsrcl 21145 |
. . . . . 6
β’ (π΅ β (OBasisβπ) β π β PreHil) |
2 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
3 | 2 | obsss 21146 |
. . . . . 6
β’ (π΅ β (OBasisβπ) β π΅ β (Baseβπ)) |
4 | | eqid 2733 |
. . . . . . 7
β’
(ocvβπ) =
(ocvβπ) |
5 | | obslbs.n |
. . . . . . 7
β’ π = (LSpanβπ) |
6 | 2, 4, 5 | ocvlsp 21096 |
. . . . . 6
β’ ((π β PreHil β§ π΅ β (Baseβπ)) β ((ocvβπ)β(πβπ΅)) = ((ocvβπ)βπ΅)) |
7 | 1, 3, 6 | syl2anc 585 |
. . . . 5
β’ (π΅ β (OBasisβπ) β ((ocvβπ)β(πβπ΅)) = ((ocvβπ)βπ΅)) |
8 | 7 | fveq2d 6847 |
. . . 4
β’ (π΅ β (OBasisβπ) β ((ocvβπ)β((ocvβπ)β(πβπ΅))) = ((ocvβπ)β((ocvβπ)βπ΅))) |
9 | 4, 2 | obs2ocv 21149 |
. . . 4
β’ (π΅ β (OBasisβπ) β ((ocvβπ)β((ocvβπ)βπ΅)) = (Baseβπ)) |
10 | 8, 9 | eqtrd 2773 |
. . 3
β’ (π΅ β (OBasisβπ) β ((ocvβπ)β((ocvβπ)β(πβπ΅))) = (Baseβπ)) |
11 | 10 | eqeq2d 2744 |
. 2
β’ (π΅ β (OBasisβπ) β ((πβπ΅) = ((ocvβπ)β((ocvβπ)β(πβπ΅))) β (πβπ΅) = (Baseβπ))) |
12 | | obslbs.c |
. . . 4
β’ πΆ = (ClSubSpβπ) |
13 | 4, 12 | iscss 21103 |
. . 3
β’ (π β PreHil β ((πβπ΅) β πΆ β (πβπ΅) = ((ocvβπ)β((ocvβπ)β(πβπ΅))))) |
14 | 1, 13 | syl 17 |
. 2
β’ (π΅ β (OBasisβπ) β ((πβπ΅) β πΆ β (πβπ΅) = ((ocvβπ)β((ocvβπ)β(πβπ΅))))) |
15 | | phllvec 21049 |
. . . 4
β’ (π β PreHil β π β LVec) |
16 | 1, 15 | syl 17 |
. . 3
β’ (π΅ β (OBasisβπ) β π β LVec) |
17 | | pssnel 4431 |
. . . . . . 7
β’ (π₯ β π΅ β βπ¦(π¦ β π΅ β§ Β¬ π¦ β π₯)) |
18 | 17 | adantl 483 |
. . . . . 6
β’ ((π΅ β (OBasisβπ) β§ π₯ β π΅) β βπ¦(π¦ β π΅ β§ Β¬ π¦ β π₯)) |
19 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π΅ β (OBasisβπ)) |
20 | | pssss 4056 |
. . . . . . . . . . . 12
β’ (π₯ β π΅ β π₯ β π΅) |
21 | 20 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π₯ β π΅) |
22 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π¦ β π΅) |
23 | 4 | obselocv 21150 |
. . . . . . . . . . 11
β’ ((π΅ β (OBasisβπ) β§ π₯ β π΅ β§ π¦ β π΅) β (π¦ β ((ocvβπ)βπ₯) β Β¬ π¦ β π₯)) |
24 | 19, 21, 22, 23 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (π¦ β ((ocvβπ)βπ₯) β Β¬ π¦ β π₯)) |
25 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(0gβπ) = (0gβπ) |
26 | 25 | obsne0 21147 |
. . . . . . . . . . . . 13
β’ ((π΅ β (OBasisβπ) β§ π¦ β π΅) β π¦ β (0gβπ)) |
27 | 19, 22, 26 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π¦ β (0gβπ)) |
28 | | nelsn 4627 |
. . . . . . . . . . . 12
β’ (π¦ β (0gβπ) β Β¬ π¦ β
{(0gβπ)}) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β Β¬ π¦ β {(0gβπ)}) |
30 | | nelne1 3038 |
. . . . . . . . . . . 12
β’ ((π¦ β ((ocvβπ)βπ₯) β§ Β¬ π¦ β {(0gβπ)}) β ((ocvβπ)βπ₯) β {(0gβπ)}) |
31 | 30 | expcom 415 |
. . . . . . . . . . 11
β’ (Β¬
π¦ β
{(0gβπ)}
β (π¦ β
((ocvβπ)βπ₯) β ((ocvβπ)βπ₯) β {(0gβπ)})) |
32 | 29, 31 | syl 17 |
. . . . . . . . . 10
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (π¦ β ((ocvβπ)βπ₯) β ((ocvβπ)βπ₯) β {(0gβπ)})) |
33 | 24, 32 | sylbird 260 |
. . . . . . . . 9
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (Β¬ π¦ β π₯ β ((ocvβπ)βπ₯) β {(0gβπ)})) |
34 | | npss 4071 |
. . . . . . . . . . 11
β’ (Β¬
(πβπ₯) β (Baseβπ) β ((πβπ₯) β (Baseβπ) β (πβπ₯) = (Baseβπ))) |
35 | | phllmod 21050 |
. . . . . . . . . . . . . . 15
β’ (π β PreHil β π β LMod) |
36 | 1, 35 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π΅ β (OBasisβπ) β π β LMod) |
37 | 36 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π β LMod) |
38 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π΅ β (Baseβπ)) |
39 | 21, 38 | sstrd 3955 |
. . . . . . . . . . . . 13
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π₯ β (Baseβπ)) |
40 | 2, 5 | lspssv 20459 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π₯ β (Baseβπ)) β (πβπ₯) β (Baseβπ)) |
41 | 37, 39, 40 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (πβπ₯) β (Baseβπ)) |
42 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ ((πβπ₯) = (Baseβπ) β ((ocvβπ)β(πβπ₯)) = ((ocvβπ)β(Baseβπ))) |
43 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β π β PreHil) |
44 | 2, 4, 5 | ocvlsp 21096 |
. . . . . . . . . . . . . . 15
β’ ((π β PreHil β§ π₯ β (Baseβπ)) β ((ocvβπ)β(πβπ₯)) = ((ocvβπ)βπ₯)) |
45 | 43, 39, 44 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β ((ocvβπ)β(πβπ₯)) = ((ocvβπ)βπ₯)) |
46 | 2, 4, 25 | ocv1 21099 |
. . . . . . . . . . . . . . 15
β’ (π β PreHil β
((ocvβπ)β(Baseβπ)) = {(0gβπ)}) |
47 | 43, 46 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β ((ocvβπ)β(Baseβπ)) = {(0gβπ)}) |
48 | 45, 47 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (((ocvβπ)β(πβπ₯)) = ((ocvβπ)β(Baseβπ)) β ((ocvβπ)βπ₯) = {(0gβπ)})) |
49 | 42, 48 | imbitrid 243 |
. . . . . . . . . . . 12
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β ((πβπ₯) = (Baseβπ) β ((ocvβπ)βπ₯) = {(0gβπ)})) |
50 | 41, 49 | embantd 59 |
. . . . . . . . . . 11
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (((πβπ₯) β (Baseβπ) β (πβπ₯) = (Baseβπ)) β ((ocvβπ)βπ₯) = {(0gβπ)})) |
51 | 34, 50 | biimtrid 241 |
. . . . . . . . . 10
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (Β¬ (πβπ₯) β (Baseβπ) β ((ocvβπ)βπ₯) = {(0gβπ)})) |
52 | 51 | necon1ad 2957 |
. . . . . . . . 9
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (((ocvβπ)βπ₯) β {(0gβπ)} β (πβπ₯) β (Baseβπ))) |
53 | 33, 52 | syld 47 |
. . . . . . . 8
β’ (((π΅ β (OBasisβπ) β§ π₯ β π΅) β§ π¦ β π΅) β (Β¬ π¦ β π₯ β (πβπ₯) β (Baseβπ))) |
54 | 53 | expimpd 455 |
. . . . . . 7
β’ ((π΅ β (OBasisβπ) β§ π₯ β π΅) β ((π¦ β π΅ β§ Β¬ π¦ β π₯) β (πβπ₯) β (Baseβπ))) |
55 | 54 | exlimdv 1937 |
. . . . . 6
β’ ((π΅ β (OBasisβπ) β§ π₯ β π΅) β (βπ¦(π¦ β π΅ β§ Β¬ π¦ β π₯) β (πβπ₯) β (Baseβπ))) |
56 | 18, 55 | mpd 15 |
. . . . 5
β’ ((π΅ β (OBasisβπ) β§ π₯ β π΅) β (πβπ₯) β (Baseβπ)) |
57 | 56 | ex 414 |
. . . 4
β’ (π΅ β (OBasisβπ) β (π₯ β π΅ β (πβπ₯) β (Baseβπ))) |
58 | 57 | alrimiv 1931 |
. . 3
β’ (π΅ β (OBasisβπ) β βπ₯(π₯ β π΅ β (πβπ₯) β (Baseβπ))) |
59 | | obslbs.j |
. . . . . 6
β’ π½ = (LBasisβπ) |
60 | 2, 59, 5 | islbs3 20632 |
. . . . 5
β’ (π β LVec β (π΅ β π½ β (π΅ β (Baseβπ) β§ (πβπ΅) = (Baseβπ) β§ βπ₯(π₯ β π΅ β (πβπ₯) β (Baseβπ))))) |
61 | | 3anan32 1098 |
. . . . 5
β’ ((π΅ β (Baseβπ) β§ (πβπ΅) = (Baseβπ) β§ βπ₯(π₯ β π΅ β (πβπ₯) β (Baseβπ))) β ((π΅ β (Baseβπ) β§ βπ₯(π₯ β π΅ β (πβπ₯) β (Baseβπ))) β§ (πβπ΅) = (Baseβπ))) |
62 | 60, 61 | bitrdi 287 |
. . . 4
β’ (π β LVec β (π΅ β π½ β ((π΅ β (Baseβπ) β§ βπ₯(π₯ β π΅ β (πβπ₯) β (Baseβπ))) β§ (πβπ΅) = (Baseβπ)))) |
63 | 62 | baibd 541 |
. . 3
β’ ((π β LVec β§ (π΅ β (Baseβπ) β§ βπ₯(π₯ β π΅ β (πβπ₯) β (Baseβπ)))) β (π΅ β π½ β (πβπ΅) = (Baseβπ))) |
64 | 16, 3, 58, 63 | syl12anc 836 |
. 2
β’ (π΅ β (OBasisβπ) β (π΅ β π½ β (πβπ΅) = (Baseβπ))) |
65 | 11, 14, 64 | 3bitr4rd 312 |
1
β’ (π΅ β (OBasisβπ) β (π΅ β π½ β (πβπ΅) β πΆ)) |