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

Metamath Proof Explorer

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 \in C_{ℋ}$
	pjsumt.2	$⊢ H \in C_{ℋ}$
Assertion	pj11i	$⊢ {proj}_{ℎ} (G) = {proj}_{ℎ} (H) \leftrightarrow G = H$

Step	Hyp	Ref	Expression
1		pjsumt.1	$⊢ G \in C_{ℋ}$
2		pjsumt.2	$⊢ H \in C_{ℋ}$
3		rneq	$⊢ {proj}_{ℎ} (G) = {proj}_{ℎ} (H) \to ran {proj}_{ℎ} (G) = ran {proj}_{ℎ} (H)$
4	1	pjrni	$⊢ ran {proj}_{ℎ} (G) = G$
5	2	pjrni	$⊢ ran {proj}_{ℎ} (H) = H$
6	3 4 5	3eqtr3g	$⊢ {proj}_{ℎ} (G) = {proj}_{ℎ} (H) \to G = H$
7		fveq2	$⊢ G = H \to {proj}_{ℎ} (G) = {proj}_{ℎ} (H)$
8	6 7	impbii	$⊢ {proj}_{ℎ} (G) = {proj}_{ℎ} (H) \leftrightarrow G = H$