Metamath Proof Explorer

Table of Contents - 10.9.3. Orthogonal projection and orthonormal bases

1. cpj
2. chil
3. cobs
4. df-pj
5. df-hil
6. df-obs
7. pjfval
8. pjdm
9. pjpm
10. pjfval2
11. pjval
12. pjdm2
13. pjff
14. pjf
15. pjf2
16. pjfo
17. pjcss
18. ocvpj
19. ishil
20. ishil2
21. isobs
22. obsip
23. obsipid
24. obsrcl
25. obsss
26. obsne0
27. obsocv
28. obs2ocv
29. obselocv
30. obs2ss
31. obslbs