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 ˙=ocvW
Assertion obselocv BOBasisWCBABA˙C¬AC

Proof

Step Hyp Ref Expression
1 obselocv.o ˙=ocvW
2 eqid 0W=0W
3 2 obsne0 BOBasisWABA0W
4 3 3adant2 BOBasisWCBABA0W
5 elin AC˙CACA˙C
6 obsrcl BOBasisWWPreHil
7 6 3ad2ant1 BOBasisWCBABWPreHil
8 phllmod WPreHilWLMod
9 7 8 syl BOBasisWCBABWLMod
10 simp2 BOBasisWCBABCB
11 eqid BaseW=BaseW
12 11 obsss BOBasisWBBaseW
13 12 3ad2ant1 BOBasisWCBABBBaseW
14 10 13 sstrd BOBasisWCBABCBaseW
15 eqid LSpanW=LSpanW
16 11 15 lspssid WLModCBaseWCLSpanWC
17 9 14 16 syl2anc BOBasisWCBABCLSpanWC
18 17 ssrind BOBasisWCBABC˙CLSpanWC˙C
19 11 1 15 ocvlsp WPreHilCBaseW˙LSpanWC=˙C
20 7 14 19 syl2anc BOBasisWCBAB˙LSpanWC=˙C
21 20 ineq2d BOBasisWCBABLSpanWC˙LSpanWC=LSpanWC˙C
22 eqid LSubSpW=LSubSpW
23 11 22 15 lspcl WLModCBaseWLSpanWCLSubSpW
24 9 14 23 syl2anc BOBasisWCBABLSpanWCLSubSpW
25 1 22 2 ocvin WPreHilLSpanWCLSubSpWLSpanWC˙LSpanWC=0W
26 7 24 25 syl2anc BOBasisWCBABLSpanWC˙LSpanWC=0W
27 21 26 eqtr3d BOBasisWCBABLSpanWC˙C=0W
28 18 27 sseqtrd BOBasisWCBABC˙C0W
29 28 sseld BOBasisWCBABAC˙CA0W
30 5 29 syl5bir BOBasisWCBABACA˙CA0W
31 elsni A0WA=0W
32 30 31 syl6 BOBasisWCBABACA˙CA=0W
33 32 necon3ad BOBasisWCBABA0W¬ACA˙C
34 4 33 mpd BOBasisWCBAB¬ACA˙C
35 imnan AC¬A˙C¬ACA˙C
36 34 35 sylibr BOBasisWCBABAC¬A˙C
37 36 con2d BOBasisWCBABA˙C¬AC
38 simpr BOBasisWCBABxCxC
39 eleq1 A=xACxC
40 38 39 syl5ibrcom BOBasisWCBABxCA=xAC
41 40 con3d BOBasisWCBABxC¬AC¬A=x
42 simpl1 BOBasisWCBABxCBOBasisW
43 simpl3 BOBasisWCBABxCAB
44 10 sselda BOBasisWCBABxCxB
45 eqid 𝑖W=𝑖W
46 eqid ScalarW=ScalarW
47 eqid 1ScalarW=1ScalarW
48 eqid 0ScalarW=0ScalarW
49 11 45 46 47 48 obsip BOBasisWABxBA𝑖Wx=ifA=x1ScalarW0ScalarW
50 42 43 44 49 syl3anc BOBasisWCBABxCA𝑖Wx=ifA=x1ScalarW0ScalarW
51 iffalse ¬A=xifA=x1ScalarW0ScalarW=0ScalarW
52 51 eqeq2d ¬A=xA𝑖Wx=ifA=x1ScalarW0ScalarWA𝑖Wx=0ScalarW
53 50 52 syl5ibcom BOBasisWCBABxC¬A=xA𝑖Wx=0ScalarW
54 41 53 syld BOBasisWCBABxC¬ACA𝑖Wx=0ScalarW
55 54 ralrimdva BOBasisWCBAB¬ACxCA𝑖Wx=0ScalarW
56 simp3 BOBasisWCBABAB
57 13 56 sseldd BOBasisWCBABABaseW
58 11 45 46 48 1 elocv A˙CCBaseWABaseWxCA𝑖Wx=0ScalarW
59 df-3an CBaseWABaseWxCA𝑖Wx=0ScalarWCBaseWABaseWxCA𝑖Wx=0ScalarW
60 58 59 bitri A˙CCBaseWABaseWxCA𝑖Wx=0ScalarW
61 60 baib CBaseWABaseWA˙CxCA𝑖Wx=0ScalarW
62 14 57 61 syl2anc BOBasisWCBABA˙CxCA𝑖Wx=0ScalarW
63 55 62 sylibrd BOBasisWCBAB¬ACA˙C
64 37 63 impbid BOBasisWCBABA˙C¬AC