Metamath Proof Explorer

Theorem obslbs

Description: An orthogonal basis is a linear basis iff the span of the basis elements is closed (which is usually not true). (Contributed by Mario Carneiro, 29-Oct-2015)

Ref Expression
Hypotheses obslbs.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
obslbs.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
obslbs.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion obslbs ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( 𝐵 ∈ 𝐽 ↔ ( 𝑁 ‘ 𝐵 ) ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 obslbs.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2 obslbs.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 obslbs.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
4 obsrcl ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝑊 ∈ PreHil )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 5 obsss ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
7 eqid ⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
8 5 7 2 ocvlsp ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ⊆ ( Base ‘ 𝑊 ) ) → ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝐵 ) ) = ( ( ocv ‘ 𝑊 ) ‘ 𝐵 ) )
9 4 6 8 syl2anc ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝐵 ) ) = ( ( ocv ‘ 𝑊 ) ‘ 𝐵 ) )
10 9 fveq2d ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝐵 ) ) ) = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝐵 ) ) )
11 7 5 obs2ocv ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝐵 ) ) = ( Base ‘ 𝑊 ) )
12 10 11 eqtrd ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝐵 ) ) ) = ( Base ‘ 𝑊 ) )
13 12 eqeq2d ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ( 𝑁 ‘ 𝐵 ) = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝐵 ) ) ) ↔ ( 𝑁 ‘ 𝐵 ) = ( Base ‘ 𝑊 ) ) )
14 7 3 iscss ⊢ ( 𝑊 ∈ PreHil → ( ( 𝑁 ‘ 𝐵 ) ∈ 𝐶 ↔ ( 𝑁 ‘ 𝐵 ) = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝐵 ) ) ) ) )
15 4 14 syl ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ( 𝑁 ‘ 𝐵 ) ∈ 𝐶 ↔ ( 𝑁 ‘ 𝐵 ) = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝐵 ) ) ) ) )
16 phllvec ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LVec )
17 4 16 syl ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝑊 ∈ LVec )
18 pssnel ⊢ ( 𝑥 ⊊ 𝐵 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥 ) )
19 18 adantl ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥 ) )
20 simpll ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐵 ∈ ( OBasis ‘ 𝑊 ) )
21 pssss ⊢ ( 𝑥 ⊊ 𝐵 → 𝑥 ⊆ 𝐵 )
22 21 ad2antlr ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ⊆ 𝐵 )
23 simpr ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
24 7 obselocv ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ↔ ¬ 𝑦 ∈ 𝑥 ) )
25 20 22 23 24 syl3anc ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ↔ ¬ 𝑦 ∈ 𝑥 ) )
26 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
27 26 obsne0 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ≠ ( 0g ‘ 𝑊 ) )
28 20 23 27 syl2anc ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ≠ ( 0g ‘ 𝑊 ) )
29 nelsn ⊢ ( 𝑦 ≠ ( 0g ‘ 𝑊 ) → ¬ 𝑦 ∈ { ( 0g ‘ 𝑊 ) } )
30 28 29 syl ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝑦 ∈ { ( 0g ‘ 𝑊 ) } )
31 nelne1 ⊢ ( ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ∧ ¬ 𝑦 ∈ { ( 0g ‘ 𝑊 ) } ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ≠ { ( 0g ‘ 𝑊 ) } )
32 31 expcom ⊢ ( ¬ 𝑦 ∈ { ( 0g ‘ 𝑊 ) } → ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ≠ { ( 0g ‘ 𝑊 ) } ) )
33 30 32 syl ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ≠ { ( 0g ‘ 𝑊 ) } ) )
34 25 33 sylbird ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑦 ∈ 𝑥 → ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ≠ { ( 0g ‘ 𝑊 ) } ) )
35 npss ⊢ ( ¬ ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ↔ ( ( 𝑁 ‘ 𝑥 ) ⊆ ( Base ‘ 𝑊 ) → ( 𝑁 ‘ 𝑥 ) = ( Base ‘ 𝑊 ) ) )
36 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
37 4 36 syl ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝑊 ∈ LMod )
38 37 ad2antrr ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ LMod )
39 6 ad2antrr ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
40 22 39 sstrd ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ⊆ ( Base ‘ 𝑊 ) )
41 5 2 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑥 ) ⊆ ( Base ‘ 𝑊 ) )
42 38 40 41 syl2anc ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑥 ) ⊆ ( Base ‘ 𝑊 ) )
43 fveq2 ⊢ ( ( 𝑁 ‘ 𝑥 ) = ( Base ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝑥 ) ) = ( ( ocv ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) )
44 4 ad2antrr ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ PreHil )
45 5 7 2 ocvlsp ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ ( Base ‘ 𝑊 ) ) → ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝑥 ) ) = ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) )
46 44 40 45 syl2anc ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝑥 ) ) = ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) )
47 5 7 26 ocv1 ⊢ ( 𝑊 ∈ PreHil → ( ( ocv ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) = { ( 0g ‘ 𝑊 ) } )
48 44 47 syl ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ocv ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) = { ( 0g ‘ 𝑊 ) } )
49 46 48 eqeq12d ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ocv ‘ 𝑊 ) ‘ ( 𝑁 ‘ 𝑥 ) ) = ( ( ocv ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) ↔ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) = { ( 0g ‘ 𝑊 ) } ) )
50 43 49 syl5ib ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑥 ) = ( Base ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) = { ( 0g ‘ 𝑊 ) } ) )
51 42 50 embantd ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑁 ‘ 𝑥 ) ⊆ ( Base ‘ 𝑊 ) → ( 𝑁 ‘ 𝑥 ) = ( Base ‘ 𝑊 ) ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) = { ( 0g ‘ 𝑊 ) } ) )
52 35 51 syl5bi ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ¬ ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) = { ( 0g ‘ 𝑊 ) } ) )
53 52 necon1ad ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ≠ { ( 0g ‘ 𝑊 ) } → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) )
54 34 53 syld ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑦 ∈ 𝑥 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) )
55 54 expimpd ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥 ) → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) )
56 55 exlimdv ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) → ( ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑥 ) → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) )
57 19 56 mpd ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥 ⊊ 𝐵 ) → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) )
58 57 ex ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( 𝑥 ⊊ 𝐵 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) )
59 58 alrimiv ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ∀ 𝑥 ( 𝑥 ⊊ 𝐵 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) )
60 5 1 2 islbs3 ⊢ ( 𝑊 ∈ LVec → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑁 ‘ 𝐵 ) = ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ( 𝑥 ⊊ 𝐵 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) ) ) )
61 3anan32 ⊢ ( ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑁 ‘ 𝐵 ) = ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ( 𝑥 ⊊ 𝐵 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) ) ↔ ( ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ( 𝑥 ⊊ 𝐵 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑁 ‘ 𝐵 ) = ( Base ‘ 𝑊 ) ) )
62 60 61 bitrdi ⊢ ( 𝑊 ∈ LVec → ( 𝐵 ∈ 𝐽 ↔ ( ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ( 𝑥 ⊊ 𝐵 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑁 ‘ 𝐵 ) = ( Base ‘ 𝑊 ) ) ) )
63 62 baibd ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ( 𝑥 ⊊ 𝐵 → ( 𝑁 ‘ 𝑥 ) ⊊ ( Base ‘ 𝑊 ) ) ) ) → ( 𝐵 ∈ 𝐽 ↔ ( 𝑁 ‘ 𝐵 ) = ( Base ‘ 𝑊 ) ) )
64 17 6 59 63 syl12anc ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( 𝐵 ∈ 𝐽 ↔ ( 𝑁 ‘ 𝐵 ) = ( Base ‘ 𝑊 ) ) )
65 13 15 64 3bitr4rd ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( 𝐵 ∈ 𝐽 ↔ ( 𝑁 ‘ 𝐵 ) ∈ 𝐶 ) )