Theorem pj11

Description: One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pj11	⊢ ( ( 𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) → ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ) )
2		eqeq1	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) → ( 𝐺 = 𝐻 ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ) )
3	1 2	bibi12d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) → ( ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 ) ↔ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ) ) )
4		fveq2	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) )
5	4	eqeq2d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ↔ ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) )
6		eqeq2	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) )
7	5 6	bibi12d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ) ↔ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) )
8		h0elch	⊢ 0ℋ ∈ Cℋ
9	8	elimel	⊢ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ∈ Cℋ
10	8	elimel	⊢ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ∈ Cℋ
11	9 10	pj11i	⊢ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) )
12	3 7 11	dedth2h	⊢ ( ( 𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 ) )