# Metamath Proof Explorer

## Theorem pjssdif2i

Description: The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of Halmos p. 48 (shortened with pjssposi ). (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjssdif2i ${⊢}{G}\subseteq {H}↔{\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)$

### Proof

Step Hyp Ref Expression
1 pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
4 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
5 hodval ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ\wedge {\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)$
6 3 4 5 mp3an12 ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)$
7 6 adantl ${⊢}\left({G}\subseteq {H}\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)$
8 2 1 pjssmi ${⊢}{x}\in ℋ\to \left({G}\subseteq {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right)\right)$
9 8 impcom ${⊢}\left({G}\subseteq {H}\wedge {x}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right)$
10 7 9 eqtrd ${⊢}\left({G}\subseteq {H}\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right)$
11 10 ralrimiva ${⊢}{G}\subseteq {H}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right)$
12 3 4 hosubfni ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)Fnℋ$
13 1 choccli ${⊢}\perp \left({G}\right)\in {\mathbf{C}}_{ℋ}$
14 2 13 chincli ${⊢}{H}\cap \perp \left({G}\right)\in {\mathbf{C}}_{ℋ}$
15 14 pjfni ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)Fnℋ$
16 eqfnfv ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)Fnℋ\wedge {\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)Fnℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right)\right)$
17 12 15 16 mp2an ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right)$
18 11 17 sylibr ${⊢}{G}\subseteq {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)$
19 14 pjige0i ${⊢}{x}\in ℋ\to 0\le {\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
20 19 adantl ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\wedge {x}\in ℋ\right)\to 0\le {\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
21 fveq1 ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right)$
22 21 oveq1d ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
23 22 adantr ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
24 20 23 breqtrrd ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\wedge {x}\in ℋ\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
25 24 ralrimiva ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}0\le \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
26 1 2 pjssposi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}0\le \left({\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔{G}\subseteq {H}$
27 25 26 sylib ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)\to {G}\subseteq {H}$
28 18 27 impbii ${⊢}{G}\subseteq {H}↔{\mathrm{proj}}_{ℎ}\left({H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap \perp \left({G}\right)\right)$