Metamath Proof Explorer

Theorem obselocv

Description: A basis element is in the orthocomplement of a subset of the basis iff it is not in the subset. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypothesis obselocv.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion obselocv ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ↔ ¬ 𝐴 ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 obselocv.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
2 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
3 2 obsne0 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ≠ ( 0g ‘ 𝑊 ) )
4 3 3adant2 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ≠ ( 0g ‘ 𝑊 ) )
5 elin ⊢ ( 𝐴 ∈ ( 𝐶 ∩ ( ⊥ ‘ 𝐶 ) ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) )
6 obsrcl ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝑊 ∈ PreHil )
7 6 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝑊 ∈ PreHil )
8 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
9 7 8 syl ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝑊 ∈ LMod )
10 simp2 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ⊆ 𝐵 )
11 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12 11 obsss ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
13 12 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
14 10 13 sstrd ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ⊆ ( Base ‘ 𝑊 ) )
15 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
16 11 15 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ⊆ ( Base ‘ 𝑊 ) ) → 𝐶 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) )
17 9 14 16 syl2anc ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) )
18 17 ssrind ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∩ ( ⊥ ‘ 𝐶 ) ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∩ ( ⊥ ‘ 𝐶 ) ) )
19 11 1 15 ocvlsp ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ⊆ ( Base ‘ 𝑊 ) ) → ( ⊥ ‘ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ) = ( ⊥ ‘ 𝐶 ) )
20 7 14 19 syl2anc ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ⊥ ‘ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ) = ( ⊥ ‘ 𝐶 ) )
21 20 ineq2d ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∩ ( ⊥ ‘ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ) ) = ( ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∩ ( ⊥ ‘ 𝐶 ) ) )
22 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
23 11 22 15 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ⊆ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∈ ( LSubSp ‘ 𝑊 ) )
24 9 14 23 syl2anc ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∈ ( LSubSp ‘ 𝑊 ) )
25 1 22 2 ocvin ⊢ ( ( 𝑊 ∈ PreHil ∧ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∩ ( ⊥ ‘ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ) ) = { ( 0g ‘ 𝑊 ) } )
26 7 24 25 syl2anc ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∩ ( ⊥ ‘ ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ) ) = { ( 0g ‘ 𝑊 ) } )
27 21 26 eqtr3d ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( ( LSpan ‘ 𝑊 ) ‘ 𝐶 ) ∩ ( ⊥ ‘ 𝐶 ) ) = { ( 0g ‘ 𝑊 ) } )
28 18 27 sseqtrd ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∩ ( ⊥ ‘ 𝐶 ) ) ⊆ { ( 0g ‘ 𝑊 ) } )
29 28 sseld ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝐶 ∩ ( ⊥ ‘ 𝐶 ) ) → 𝐴 ∈ { ( 0g ‘ 𝑊 ) } ) )
30 5 29 biimtrrid ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) → 𝐴 ∈ { ( 0g ‘ 𝑊 ) } ) )
31 elsni ⊢ ( 𝐴 ∈ { ( 0g ‘ 𝑊 ) } → 𝐴 = ( 0g ‘ 𝑊 ) )
32 30 31 syl6 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) → 𝐴 = ( 0g ‘ 𝑊 ) ) )
33 32 necon3ad ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ≠ ( 0g ‘ 𝑊 ) → ¬ ( 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) ) )
34 4 33 mpd ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ¬ ( 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) )
35 imnan ⊢ ( ( 𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) ↔ ¬ ( 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) )
36 34 35 sylibr ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) )
37 36 con2d ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐶 ) → ¬ 𝐴 ∈ 𝐶 ) )
38 simpr ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
39 eleq1 ⊢ ( 𝐴 = 𝑥 → ( 𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶 ) )
40 38 39 syl5ibrcom ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐴 = 𝑥 → 𝐴 ∈ 𝐶 ) )
41 40 con3d ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → ( ¬ 𝐴 ∈ 𝐶 → ¬ 𝐴 = 𝑥 ) )
42 simpl1 ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ ( OBasis ‘ 𝑊 ) )
43 simpl3 ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
44 10 sselda ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐵 )
45 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
46 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
47 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
48 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
49 11 45 46 47 48 obsip ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = if ( 𝐴 = 𝑥 , ( 1r ‘ ( Scalar ‘ 𝑊 ) ) , ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
50 42 43 44 49 syl3anc ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = if ( 𝐴 = 𝑥 , ( 1r ‘ ( Scalar ‘ 𝑊 ) ) , ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
51 iffalse ⊢ ( ¬ 𝐴 = 𝑥 → if ( 𝐴 = 𝑥 , ( 1r ‘ ( Scalar ‘ 𝑊 ) ) , ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
52 51 eqeq2d ⊢ ( ¬ 𝐴 = 𝑥 → ( ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = if ( 𝐴 = 𝑥 , ( 1r ‘ ( Scalar ‘ 𝑊 ) ) , ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
53 50 52 syl5ibcom ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → ( ¬ 𝐴 = 𝑥 → ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
54 41 53 syld ⊢ ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → ( ¬ 𝐴 ∈ 𝐶 → ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
55 54 ralrimdva ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ 𝐶 → ∀ 𝑥 ∈ 𝐶 ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
56 simp3 ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
57 13 56 sseldd ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ( Base ‘ 𝑊 ) )
58 11 45 46 48 1 elocv ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ↔ ( 𝐶 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐴 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐶 ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
59 df-3an ⊢ ( ( 𝐶 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐴 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐶 ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( ( 𝐶 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐴 ∈ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐶 ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
60 58 59 bitri ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ↔ ( ( 𝐶 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐴 ∈ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐶 ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
61 60 baib ⊢ ( ( 𝐶 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐴 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐶 ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
62 14 57 61 syl2anc ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐶 ( 𝐴 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
63 55 62 sylibrd ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ 𝐶 → 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ) )
64 37 63 impbid ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐶 ) ↔ ¬ 𝐴 ∈ 𝐶 ) )