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	⊢ 𝐺 ∈ C_ℋ
		pjco.2	⊢ 𝐻 ∈ C_ℋ
	Assertion	pjssge0i	⊢ ( 𝐴 ∈ ℋ → ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( proj_ℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ) )

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		id	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) )
9	5 8	oveq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) = ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) )
10	9	breq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ↔ 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
11	7 10	imbi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( proj_ℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ) ↔ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) = ( ( proj_ℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) → 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ) )
12		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ℋ
13	2 12 1	pjssge0ii	⊢ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) = ( ( proj_ℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) → 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) )
14	11 13	dedth	⊢ ( 𝐴 ∈ ℋ → ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( proj_ℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ) )