Theorem pj11i

Description: One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjsumt.1	⊢ 𝐺 ∈ Cℋ
	pjsumt.2	⊢ 𝐻 ∈ Cℋ
Assertion	pj11i	⊢ ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		pjsumt.1	⊢ 𝐺 ∈ Cℋ
2		pjsumt.2	⊢ 𝐻 ∈ Cℋ
3		rneq	⊢ ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) → ran ( projℎ ‘ 𝐺 ) = ran ( projℎ ‘ 𝐻 ) )
4	1	pjrni	⊢ ran ( projℎ ‘ 𝐺 ) = 𝐺
5	2	pjrni	⊢ ran ( projℎ ‘ 𝐻 ) = 𝐻
6	3 4 5	3eqtr3g	⊢ ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) → 𝐺 = 𝐻 )
7		fveq2	⊢ ( 𝐺 = 𝐻 → ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) )
8	6 7	impbii	⊢ ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 )