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	|- G e. CH
	pjsumt.2	|- H e. CH
Assertion	pj11i	|- ( ( projh ` G ) = ( projh ` H ) <-> G = H )

Proof

Step	Hyp	Ref	Expression
1		pjsumt.1	|- G e. CH
2		pjsumt.2	|- H e. CH
3		rneq	|- ( ( projh ` G ) = ( projh ` H ) -> ran ( projh ` G ) = ran ( projh ` H ) )
4	1	pjrni	|- ran ( projh ` G ) = G
5	2	pjrni	|- ran ( projh ` H ) = H
6	3 4 5	3eqtr3g	|- ( ( projh ` G ) = ( projh ` H ) -> G = H )
7		fveq2	|- ( G = H -> ( projh ` G ) = ( projh ` H ) )
8	6 7	impbii	|- ( ( projh ` G ) = ( projh ` H ) <-> G = H )