Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ocvin Structured version   Unicode version

Theorem ocvin 16893
 Description: An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015.)
Hypotheses
Ref Expression
ocv2ss.o
ocvin.l
ocvin.z
Assertion
Ref Expression
ocvin

Proof of Theorem ocvin
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2435 . . . . . . . . 9
2 eqid 2435 . . . . . . . . 9
3 eqid 2435 . . . . . . . . 9 Scalar Scalar
4 eqid 2435 . . . . . . . . 9 Scalar Scalar
5 ocv2ss.o . . . . . . . . 9
61, 2, 3, 4, 5ocvi 16888 . . . . . . . 8 Scalar
76ancoms 440 . . . . . . 7 Scalar
87adantl 453 . . . . . 6 Scalar
9 simpll 731 . . . . . . 7
10 ocvin.l . . . . . . . . 9
111, 10lssel 16006 . . . . . . . 8
1211ad2ant2lr 729 . . . . . . 7
13 ocvin.z . . . . . . . 8
143, 2, 1, 4, 13ipeq0 16861 . . . . . . 7 Scalar
159, 12, 14syl2anc 643 . . . . . 6 Scalar
168, 15mpbid 202 . . . . 5
1716ex 424 . . . 4
18 elin 3522 . . . 4
19 elsn 3821 . . . 4
2017, 18, 193imtr4g 262 . . 3
2120ssrdv 3346 . 2
22 phllmod 16853 . . . 4