Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  pjadjii Unicode version

 Description: A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
Hypotheses
Ref Expression
pjidm.1
pjidm.2
Assertion
Ref Expression

StepHypRef Expression
1 pjidm.1 . . . . . . . 8
2 pjadj.3 . . . . . . . . 9
3 pjidm.2 . . . . . . . . 9
42, 3pjorthi 22248 . . . . . . . 8
51, 4ax-mp 8 . . . . . . 7
65fveq2i 5528 . . . . . 6
7 cj0 11643 . . . . . 6
86, 7eqtri 2303 . . . . 5
91choccli 21886 . . . . . . 7
109, 3pjhclii 22001 . . . . . 6
111, 2pjhclii 22001 . . . . . 6
1210, 11his1i 21679 . . . . 5
133, 2pjorthi 22248 . . . . . 6
141, 13ax-mp 8 . . . . 5
158, 12, 143eqtr4ri 2314 . . . 4
1615oveq2i 5869 . . 3
171, 3pjhclii 22001 . . . 4
189, 2pjhclii 22001 . . . 4
19 his7 21669 . . . 4
2017, 11, 18, 19mp3an 1277 . . 3
21 ax-his2 21662 . . . 4
2217, 10, 11, 21mp3an 1277 . . 3
2316, 20, 223eqtr4i 2313 . 2
241, 2pjpji 22003 . . 3
2524oveq2i 5869 . 2
261, 3pjpji 22003 . . 3
2726oveq1i 5868 . 2
2823, 25, 273eqtr4i 2313 1