# Metamath Proof Explorer

## Theorem pjssge0i

Description: Theorem 4.5(iv)->(v) of Beran p. 112. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjssge0i ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right)$

### Proof

Step Hyp Ref Expression
1 pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
4 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
5 3 4 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
6 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
7 5 6 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
8 id ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
9 5 8 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}=\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
10 9 breq2d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}↔0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
11 7 10 imbi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right)↔\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
12 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
13 2 12 1 pjssge0ii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
14 11 13 dedth ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right)$