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ℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) )