# Metamath Proof Explorer

## Theorem pjssmi

Description: Projection meet property. Remark in Kalmbach p. 66. Also Theorem 4.5(i)->(iv) 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 pjssmi ${⊢}{A}\in ℋ\to \left({H}\subseteq {G}\to {\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)\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 7 imbi2d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({H}\subseteq {G}\to {\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)\right)↔\left({H}\subseteq {G}\to {\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)\right)$
9 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
10 2 9 1 pjssmii ${⊢}{H}\subseteq {G}\to {\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)$
11 8 10 dedth ${⊢}{A}\in ℋ\to \left({H}\subseteq {G}\to {\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)\right)$