Metamath Proof Explorer

Theorem pjdifnormi

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

		Ref	Expression
	Hypotheses	pjco.1	⊢ 𝐺 ∈ C_ℋ
		pjco.2	⊢ 𝐻 ∈ C_ℋ
	Assertion	pjdifnormi	⊢ ( 𝐴 ∈ ℋ → ( 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ↔ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( norm_ℎ ‘ ( ( 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		id	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) )
7	5 6	oveq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) = ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) )
8	7	breq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ↔ 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
9		2fveq3	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
10		2fveq3	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
11	9 10	breq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↔ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ≤ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ) )
12	8 11	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ↔ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) ↔ ( 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ↔ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ≤ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ) ) )
13		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ℋ
14	2 13 1	pjdifnormii	⊢ ( 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ·_ih if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ↔ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) ≤ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
15	12 14	dedth	⊢ ( 𝐴 ∈ ℋ → ( 0 ≤ ( ( ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) −_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·_ih 𝐴 ) ↔ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( norm_ℎ ‘ ( ( proj_ℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) )