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 0C
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𝐻 ) ↔ 𝐺 = 𝐻 ) )