Theorem hmopidmpji

Description: An idempotent Hermitian operator is a projection operator. Theorem 26.4 of Halmos p. 44. (Halmos seems to omit the proof that H is a closed subspace, which is not trivial as hmopidmchi shows.) (Contributed by NM, 22-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hmopidmch.1	⊢ 𝑇 ∈ HrmOp
	hmopidmch.2	⊢ ( 𝑇 ∘ 𝑇 ) = 𝑇
Assertion	hmopidmpji	⊢ 𝑇 = ( projℎ ‘ ran 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		hmopidmch.1	⊢ 𝑇 ∈ HrmOp
2		hmopidmch.2	⊢ ( 𝑇 ∘ 𝑇 ) = 𝑇
3		hmoplin	⊢ ( 𝑇 ∈ HrmOp → 𝑇 ∈ LinOp )
4	1 3	ax-mp	⊢ 𝑇 ∈ LinOp
5	4	lnopfi	⊢ 𝑇 : ℋ ⟶ ℋ
6		ffn	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
7	5 6	ax-mp	⊢ 𝑇 Fn ℋ
8	1 2	hmopidmchi	⊢ ran 𝑇 ∈ Cℋ
9	8	pjfni	⊢ ( projℎ ‘ ran 𝑇 ) Fn ℋ
10		eqfnfv	⊢ ( ( 𝑇 Fn ℋ ∧ ( projℎ ‘ ran 𝑇 ) Fn ℋ ) → ( 𝑇 = ( projℎ ‘ ran 𝑇 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( ( projℎ ‘ ran 𝑇 ) ‘ 𝑥 ) ) )
11	7 9 10	mp2an	⊢ ( 𝑇 = ( projℎ ‘ ran 𝑇 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( ( projℎ ‘ ran 𝑇 ) ‘ 𝑥 ) )
12		fnfvelrn	⊢ ( ( 𝑇 Fn ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ran 𝑇 )
13	7 12	mpan	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ran 𝑇 )
14		id	⊢ ( 𝑥 ∈ ℋ → 𝑥 ∈ ℋ )
15	5	ffvelcdmi	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
16		hvsubcl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
17	14 15 16	syl2anc	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
18		simpl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → 𝑥 ∈ ℋ )
19	15	adantr	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
20	5	ffvelcdmi	⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
21	20	adantl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
22		his2sub	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) − ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) ) )
23	18 19 21 22	syl3anc	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) − ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) ) )
24		hmop	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
25	1 24	mp3an1	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
26	20 25	sylan2	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
27	5 5	hocoi	⊢ ( 𝑦 ∈ ℋ → ( ( 𝑇 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) )
28	2	fveq1i	⊢ ( ( 𝑇 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 )
29	27 28	eqtr3di	⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑇 ‘ 𝑦 ) )
30	29	adantl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑇 ‘ 𝑦 ) )
31	30	oveq2d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) )
32	26 31	eqtr3d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) )
33	32	oveq2d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) − ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) − ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) )
34		hicl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℂ )
35	20 34	sylan2	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℂ )
36	35	subidd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) − ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) = 0 )
37	23 33 36	3eqtrd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = 0 )
38	37	ralrimiva	⊢ ( 𝑥 ∈ ℋ → ∀ 𝑦 ∈ ℋ ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = 0 )
39		oveq2	⊢ ( 𝑧 = ( 𝑇 ‘ 𝑦 ) → ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑧 ) = ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
40	39	eqeq1d	⊢ ( 𝑧 = ( 𝑇 ‘ 𝑦 ) → ( ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑧 ) = 0 ↔ ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = 0 ) )
41	40	ralrn	⊢ ( 𝑇 Fn ℋ → ( ∀ 𝑧 ∈ ran 𝑇 ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑧 ) = 0 ↔ ∀ 𝑦 ∈ ℋ ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = 0 ) )
42	7 41	ax-mp	⊢ ( ∀ 𝑧 ∈ ran 𝑇 ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑧 ) = 0 ↔ ∀ 𝑦 ∈ ℋ ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = 0 )
43	38 42	sylibr	⊢ ( 𝑥 ∈ ℋ → ∀ 𝑧 ∈ ran 𝑇 ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑧 ) = 0 )
44	8	chssii	⊢ ran 𝑇 ⊆ ℋ
45		ocel	⊢ ( ran 𝑇 ⊆ ℋ → ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ran 𝑇 ) ↔ ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ∧ ∀ 𝑧 ∈ ran 𝑇 ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑧 ) = 0 ) ) )
46	44 45	ax-mp	⊢ ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ran 𝑇 ) ↔ ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ∧ ∀ 𝑧 ∈ ran 𝑇 ( ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑧 ) = 0 ) )
47	17 43 46	sylanbrc	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ran 𝑇 ) )
48	8	pjcompi	⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ ran 𝑇 ∧ ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ran 𝑇 ) ) → ( ( projℎ ‘ ran 𝑇 ) ‘ ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) = ( 𝑇 ‘ 𝑥 ) )
49	13 47 48	syl2anc	⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ran 𝑇 ) ‘ ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) = ( 𝑇 ‘ 𝑥 ) )
50		hvpncan3	⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ) = 𝑥 )
51	15 14 50	syl2anc	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ) = 𝑥 )
52	51	fveq2d	⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ran 𝑇 ) ‘ ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) = ( ( projℎ ‘ ran 𝑇 ) ‘ 𝑥 ) )
53	49 52	eqtr3d	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) = ( ( projℎ ‘ ran 𝑇 ) ‘ 𝑥 ) )
54	11 53	mprgbir	⊢ 𝑇 = ( projℎ ‘ ran 𝑇 )