| Step | Hyp | Ref
| Expression |
| 1 | | obsrcl 21743 |
. . . . . 6
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝑊 ∈ PreHil) |
| 2 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 3 | 2 | obsss 21744 |
. . . . . 6
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝐵 ⊆ (Base‘𝑊)) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢
(ocv‘𝑊) =
(ocv‘𝑊) |
| 5 | | obslbs.n |
. . . . . . 7
⊢ 𝑁 = (LSpan‘𝑊) |
| 6 | 2, 4, 5 | ocvlsp 21694 |
. . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ 𝐵 ⊆ (Base‘𝑊)) → ((ocv‘𝑊)‘(𝑁‘𝐵)) = ((ocv‘𝑊)‘𝐵)) |
| 7 | 1, 3, 6 | syl2anc 584 |
. . . . 5
⊢ (𝐵 ∈ (OBasis‘𝑊) → ((ocv‘𝑊)‘(𝑁‘𝐵)) = ((ocv‘𝑊)‘𝐵)) |
| 8 | 7 | fveq2d 6910 |
. . . 4
⊢ (𝐵 ∈ (OBasis‘𝑊) → ((ocv‘𝑊)‘((ocv‘𝑊)‘(𝑁‘𝐵))) = ((ocv‘𝑊)‘((ocv‘𝑊)‘𝐵))) |
| 9 | 4, 2 | obs2ocv 21747 |
. . . 4
⊢ (𝐵 ∈ (OBasis‘𝑊) → ((ocv‘𝑊)‘((ocv‘𝑊)‘𝐵)) = (Base‘𝑊)) |
| 10 | 8, 9 | eqtrd 2777 |
. . 3
⊢ (𝐵 ∈ (OBasis‘𝑊) → ((ocv‘𝑊)‘((ocv‘𝑊)‘(𝑁‘𝐵))) = (Base‘𝑊)) |
| 11 | 10 | eqeq2d 2748 |
. 2
⊢ (𝐵 ∈ (OBasis‘𝑊) → ((𝑁‘𝐵) = ((ocv‘𝑊)‘((ocv‘𝑊)‘(𝑁‘𝐵))) ↔ (𝑁‘𝐵) = (Base‘𝑊))) |
| 12 | | obslbs.c |
. . . 4
⊢ 𝐶 = (ClSubSp‘𝑊) |
| 13 | 4, 12 | iscss 21701 |
. . 3
⊢ (𝑊 ∈ PreHil → ((𝑁‘𝐵) ∈ 𝐶 ↔ (𝑁‘𝐵) = ((ocv‘𝑊)‘((ocv‘𝑊)‘(𝑁‘𝐵))))) |
| 14 | 1, 13 | syl 17 |
. 2
⊢ (𝐵 ∈ (OBasis‘𝑊) → ((𝑁‘𝐵) ∈ 𝐶 ↔ (𝑁‘𝐵) = ((ocv‘𝑊)‘((ocv‘𝑊)‘(𝑁‘𝐵))))) |
| 15 | | phllvec 21647 |
. . . 4
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec) |
| 16 | 1, 15 | syl 17 |
. . 3
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝑊 ∈ LVec) |
| 17 | | pssnel 4471 |
. . . . . . 7
⊢ (𝑥 ⊊ 𝐵 → ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥)) |
| 18 | 17 | adantl 481 |
. . . . . 6
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) → ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥)) |
| 19 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝐵 ∈ (OBasis‘𝑊)) |
| 20 | | pssss 4098 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊊ 𝐵 → 𝑥 ⊆ 𝐵) |
| 21 | 20 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑥 ⊆ 𝐵) |
| 22 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
| 23 | 4 | obselocv 21748 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ ((ocv‘𝑊)‘𝑥) ↔ ¬ 𝑦 ∈ 𝑥)) |
| 24 | 19, 21, 22, 23 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ ((ocv‘𝑊)‘𝑥) ↔ ¬ 𝑦 ∈ 𝑥)) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 26 | 25 | obsne0 21745 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑦 ∈ 𝐵) → 𝑦 ≠ (0g‘𝑊)) |
| 27 | 19, 22, 26 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑦 ≠ (0g‘𝑊)) |
| 28 | | nelsn 4666 |
. . . . . . . . . . . 12
⊢ (𝑦 ≠ (0g‘𝑊) → ¬ 𝑦 ∈
{(0g‘𝑊)}) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦 ∈ {(0g‘𝑊)}) |
| 30 | | nelne1 3039 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ((ocv‘𝑊)‘𝑥) ∧ ¬ 𝑦 ∈ {(0g‘𝑊)}) → ((ocv‘𝑊)‘𝑥) ≠ {(0g‘𝑊)}) |
| 31 | 30 | expcom 413 |
. . . . . . . . . . 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 4113 |
. . . . . . . . . . 11
⊢ (¬
(𝑁‘𝑥) ⊊ (Base‘𝑊) ↔ ((𝑁‘𝑥) ⊆ (Base‘𝑊) → (𝑁‘𝑥) = (Base‘𝑊))) |
| 35 | | phllmod 21648 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
| 36 | 1, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝑊 ∈ LMod) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑊 ∈ LMod) |
| 38 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝐵 ⊆ (Base‘𝑊)) |
| 39 | 21, 38 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑥 ⊆ (Base‘𝑊)) |
| 40 | 2, 5 | lspssv 20981 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ⊆ (Base‘𝑊)) → (𝑁‘𝑥) ⊆ (Base‘𝑊)) |
| 41 | 37, 39, 40 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑁‘𝑥) ⊆ (Base‘𝑊)) |
| 42 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ ((𝑁‘𝑥) = (Base‘𝑊) → ((ocv‘𝑊)‘(𝑁‘𝑥)) = ((ocv‘𝑊)‘(Base‘𝑊))) |
| 43 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑊 ∈ PreHil) |
| 44 | 2, 4, 5 | ocvlsp 21694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ PreHil ∧ 𝑥 ⊆ (Base‘𝑊)) → ((ocv‘𝑊)‘(𝑁‘𝑥)) = ((ocv‘𝑊)‘𝑥)) |
| 45 | 43, 39, 44 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((ocv‘𝑊)‘(𝑁‘𝑥)) = ((ocv‘𝑊)‘𝑥)) |
| 46 | 2, 4, 25 | ocv1 21697 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ PreHil →
((ocv‘𝑊)‘(Base‘𝑊)) = {(0g‘𝑊)}) |
| 47 | 43, 46 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((ocv‘𝑊)‘(Base‘𝑊)) = {(0g‘𝑊)}) |
| 48 | 45, 47 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → (((ocv‘𝑊)‘(𝑁‘𝑥)) = ((ocv‘𝑊)‘(Base‘𝑊)) ↔ ((ocv‘𝑊)‘𝑥) = {(0g‘𝑊)})) |
| 49 | 42, 48 | imbitrid 244 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((𝑁‘𝑥) = (Base‘𝑊) → ((ocv‘𝑊)‘𝑥) = {(0g‘𝑊)})) |
| 50 | 41, 49 | embantd 59 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) ∧ 𝑦 ∈ 𝐵) → (((𝑁‘𝑥) ⊆ (Base‘𝑊) → (𝑁‘𝑥) = (Base‘𝑊)) → ((ocv‘𝑊)‘𝑥) = {(0g‘𝑊)})) |
| 51 | 34, 50 | biimtrid 242 |
. . . . . . . . . 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 453 |
. . . . . . 7
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) → ((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥) → (𝑁‘𝑥) ⊊ (Base‘𝑊))) |
| 55 | 54 | exlimdv 1933 |
. . . . . 6
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) → (∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥) → (𝑁‘𝑥) ⊊ (Base‘𝑊))) |
| 56 | 18, 55 | mpd 15 |
. . . . 5
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝑥 ⊊ 𝐵) → (𝑁‘𝑥) ⊊ (Base‘𝑊)) |
| 57 | 56 | ex 412 |
. . . 4
⊢ (𝐵 ∈ (OBasis‘𝑊) → (𝑥 ⊊ 𝐵 → (𝑁‘𝑥) ⊊ (Base‘𝑊))) |
| 58 | 57 | alrimiv 1927 |
. . 3
⊢ (𝐵 ∈ (OBasis‘𝑊) → ∀𝑥(𝑥 ⊊ 𝐵 → (𝑁‘𝑥) ⊊ (Base‘𝑊))) |
| 59 | | obslbs.j |
. . . . . 6
⊢ 𝐽 = (LBasis‘𝑊) |
| 60 | 2, 59, 5 | islbs3 21157 |
. . . . 5
⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ (Base‘𝑊) ∧ (𝑁‘𝐵) = (Base‘𝑊) ∧ ∀𝑥(𝑥 ⊊ 𝐵 → (𝑁‘𝑥) ⊊ (Base‘𝑊))))) |
| 61 | | 3anan32 1097 |
. . . . 5
⊢ ((𝐵 ⊆ (Base‘𝑊) ∧ (𝑁‘𝐵) = (Base‘𝑊) ∧ ∀𝑥(𝑥 ⊊ 𝐵 → (𝑁‘𝑥) ⊊ (Base‘𝑊))) ↔ ((𝐵 ⊆ (Base‘𝑊) ∧ ∀𝑥(𝑥 ⊊ 𝐵 → (𝑁‘𝑥) ⊊ (Base‘𝑊))) ∧ (𝑁‘𝐵) = (Base‘𝑊))) |
| 62 | 60, 61 | bitrdi 287 |
. . . 4
⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ ((𝐵 ⊆ (Base‘𝑊) ∧ ∀𝑥(𝑥 ⊊ 𝐵 → (𝑁‘𝑥) ⊊ (Base‘𝑊))) ∧ (𝑁‘𝐵) = (Base‘𝑊)))) |
| 63 | 62 | baibd 539 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐵 ⊆ (Base‘𝑊) ∧ ∀𝑥(𝑥 ⊊ 𝐵 → (𝑁‘𝑥) ⊊ (Base‘𝑊)))) → (𝐵 ∈ 𝐽 ↔ (𝑁‘𝐵) = (Base‘𝑊))) |
| 64 | 16, 3, 58, 63 | syl12anc 837 |
. 2
⊢ (𝐵 ∈ (OBasis‘𝑊) → (𝐵 ∈ 𝐽 ↔ (𝑁‘𝐵) = (Base‘𝑊))) |
| 65 | 11, 14, 64 | 3bitr4rd 312 |
1
⊢ (𝐵 ∈ (OBasis‘𝑊) → (𝐵 ∈ 𝐽 ↔ (𝑁‘𝐵) ∈ 𝐶)) |