# 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 𝐺C
pjco.2 𝐻C
Assertion pjssmi ( 𝐴 ∈ ℋ → ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) )

### Proof

Step Hyp Ref Expression
1 pjco.1 𝐺C
2 pjco.2 𝐻C
3 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( proj𝐺 ) ‘ 𝐴 ) = ( ( proj𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
4 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( proj𝐻 ) ‘ 𝐴 ) = ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
5 3 4 oveq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( ( proj𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
6 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
7 5 6 eqeq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ↔ ( ( ( proj𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
8 7 imbi2d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ↔ ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) )
9 ifhvhv0 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ∈ ℋ
10 2 9 1 pjssmii ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
11 8 10 dedth ( 𝐴 ∈ ℋ → ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) )