This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 ) )