elpjrn

Description: Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	elpjrn	$⊢ T \in ran {proj}_{ℎ} \to ran T = \{x \in ℋ \| T (x) = x\}$

Proof

Step	Hyp	Ref	Expression
1		elpjch	$⊢ T \in ran {proj}_{ℎ} \to (ran T \in C_{ℋ} \land T = {proj}_{ℎ} (ran T))$
2	1	simpld	$⊢ T \in ran {proj}_{ℎ} \to ran T \in C_{ℋ}$
3		chss	$⊢ ran T \in C_{ℋ} \to ran T \subseteq ℋ$
4	2 3	syl	$⊢ T \in ran {proj}_{ℎ} \to ran T \subseteq ℋ$
5	4	sseld	$⊢ T \in ran {proj}_{ℎ} \to (x \in ran T \to x \in ℋ)$
6		elpjhmop	$⊢ T \in ran {proj}_{ℎ} \to T \in HrmOp$
7		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
8	6 7	syl	$⊢ T \in ran {proj}_{ℎ} \to T : ℋ ⟶ ℋ$
9	8	ffnd	$⊢ T \in ran {proj}_{ℎ} \to T Fn ℋ$
10		fvelrnb	$⊢ T Fn ℋ \to (x \in ran T \leftrightarrow \exists y \in ℋ T (y) = x)$
11	9 10	syl	$⊢ T \in ran {proj}_{ℎ} \to (x \in ran T \leftrightarrow \exists y \in ℋ T (y) = x)$
12		fvco3	$⊢ (T : ℋ ⟶ ℋ \land y \in ℋ) \to (T \circ T) (y) = T (T (y))$
13	8 12	sylan	$⊢ (T \in ran {proj}_{ℎ} \land y \in ℋ) \to (T \circ T) (y) = T (T (y))$
14		elpjidm	$⊢ T \in ran {proj}_{ℎ} \to T \circ T = T$
15	14	adantr	$⊢ (T \in ran {proj}_{ℎ} \land y \in ℋ) \to T \circ T = T$
16	15	fveq1d	$⊢ (T \in ran {proj}_{ℎ} \land y \in ℋ) \to (T \circ T) (y) = T (y)$
17	13 16	eqtr3d	$⊢ (T \in ran {proj}_{ℎ} \land y \in ℋ) \to T (T (y)) = T (y)$
18		fveq2	$⊢ T (y) = x \to T (T (y)) = T (x)$
19		id	$⊢ T (y) = x \to T (y) = x$
20	18 19	eqeq12d	$⊢ T (y) = x \to (T (T (y)) = T (y) \leftrightarrow T (x) = x)$
21	17 20	syl5ibcom	$⊢ (T \in ran {proj}_{ℎ} \land y \in ℋ) \to (T (y) = x \to T (x) = x)$
22	21	rexlimdva	$⊢ T \in ran {proj}_{ℎ} \to (\exists y \in ℋ T (y) = x \to T (x) = x)$
23	11 22	sylbid	$⊢ T \in ran {proj}_{ℎ} \to (x \in ran T \to T (x) = x)$
24	5 23	jcad	$⊢ T \in ran {proj}_{ℎ} \to (x \in ran T \to (x \in ℋ \land T (x) = x))$
25		fnfvelrn	$⊢ (T Fn ℋ \land x \in ℋ) \to T (x) \in ran T$
26	9 25	sylan	$⊢ (T \in ran {proj}_{ℎ} \land x \in ℋ) \to T (x) \in ran T$
27		eleq1	$⊢ T (x) = x \to (T (x) \in ran T \leftrightarrow x \in ran T)$
28	26 27	syl5ibcom	$⊢ (T \in ran {proj}_{ℎ} \land x \in ℋ) \to (T (x) = x \to x \in ran T)$
29	28	expimpd	$⊢ T \in ran {proj}_{ℎ} \to ((x \in ℋ \land T (x) = x) \to x \in ran T)$
30	24 29	impbid	$⊢ T \in ran {proj}_{ℎ} \to (x \in ran T \leftrightarrow (x \in ℋ \land T (x) = x))$
31	30	eqabdv	$⊢ T \in ran {proj}_{ℎ} \to ran T = \{x \| (x \in ℋ \land T (x) = x)\}$
32		df-rab	$⊢ \{x \in ℋ \| T (x) = x\} = \{x \| (x \in ℋ \land T (x) = x)\}$
33	31 32	eqtr4di	$⊢ T \in ran {proj}_{ℎ} \to ran T = \{x \in ℋ \| T (x) = x\}$

Metamath Proof Explorer

Theorem elpjrn

Proof