hmopidmch

Description: An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of AkhiezerGlazman p. 64. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hmopidmch	$⊢ (T \in HrmOp \land T \circ T = T) \to ran T \in C_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		rneq	$⊢ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to ran T = ran if ((T \in HrmOp \land T \circ T = T), T, I_{op})$
2	1	eleq1d	$⊢ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to (ran T \in C_{ℋ} \leftrightarrow ran if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in C_{ℋ})$
3		eleq1	$⊢ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to (T \in HrmOp \leftrightarrow if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in HrmOp)$
4		id	$⊢ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to T = if ((T \in HrmOp \land T \circ T = T), T, I_{op})$
5	4 4	coeq12d	$⊢ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to T \circ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op})$
6	5 4	eqeq12d	$⊢ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to (T \circ T = T \leftrightarrow if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) = if ((T \in HrmOp \land T \circ T = T), T, I_{op}))$
7	3 6	anbi12d	$⊢ T = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to ((T \in HrmOp \land T \circ T = T) \leftrightarrow (if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in HrmOp \land if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) = if ((T \in HrmOp \land T \circ T = T), T, I_{op})))$
8		eleq1	$⊢ I_{op} = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to (I_{op} \in HrmOp \leftrightarrow if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in HrmOp)$
9		id	$⊢ I_{op} = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to I_{op} = if ((T \in HrmOp \land T \circ T = T), T, I_{op})$
10	9 9	coeq12d	$⊢ I_{op} = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to I_{op} \circ I_{op} = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op})$
11	10 9	eqeq12d	$⊢ I_{op} = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to (I_{op} \circ I_{op} = I_{op} \leftrightarrow if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) = if ((T \in HrmOp \land T \circ T = T), T, I_{op}))$
12	8 11	anbi12d	$⊢ I_{op} = if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \to ((I_{op} \in HrmOp \land I_{op} \circ I_{op} = I_{op}) \leftrightarrow (if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in HrmOp \land if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) = if ((T \in HrmOp \land T \circ T = T), T, I_{op})))$
13		idhmop	$⊢ I_{op} \in HrmOp$
14		hoif	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ$
15		f1of	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ \to I_{op} : ℋ ⟶ ℋ$
16	14 15	ax-mp	$⊢ I_{op} : ℋ ⟶ ℋ$
17	16	hoid1i	$⊢ I_{op} \circ I_{op} = I_{op}$
18	13 17	pm3.2i	$⊢ (I_{op} \in HrmOp \land I_{op} \circ I_{op} = I_{op})$
19	7 12 18	elimhyp	$⊢ (if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in HrmOp \land if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) = if ((T \in HrmOp \land T \circ T = T), T, I_{op}))$
20	19	simpli	$⊢ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in HrmOp$
21	19	simpri	$⊢ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \circ if ((T \in HrmOp \land T \circ T = T), T, I_{op}) = if ((T \in HrmOp \land T \circ T = T), T, I_{op})$
22	20 21	hmopidmchi	$⊢ ran if ((T \in HrmOp \land T \circ T = T), T, I_{op}) \in C_{ℋ}$
23	2 22	dedth	$⊢ (T \in HrmOp \land T \circ T = T) \to ran T \in C_{ℋ}$

Metamath Proof Explorer

Theorem hmopidmch

Proof