Metamath Proof Explorer

Theorem 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 ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) → ran 𝑇 ∈ Cℋ )

Proof

Step Hyp Ref Expression
1 rneq ⊢ ( 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ran 𝑇 = ran if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) )
2 1 eleq1d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( ran 𝑇 ∈ Cℋ ↔ ran if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ Cℋ ) )
3 eleq1 ⊢ ( 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( 𝑇 ∈ HrmOp ↔ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ HrmOp ) )
4 id ⊢ ( 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) )
5 4 4 coeq12d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( 𝑇 ∘ 𝑇 ) = ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) )
6 5 4 eqeq12d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( ( 𝑇 ∘ 𝑇 ) = 𝑇 ↔ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) )
7 3 6 anbi12d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) ↔ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ HrmOp ∧ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) ) )
8 eleq1 ⊢ ( Iop = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( Iop ∈ HrmOp ↔ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ HrmOp ) )
9 id ⊢ ( Iop = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → Iop = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) )
10 9 9 coeq12d ⊢ ( Iop = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( Iop ∘ Iop ) = ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) )
11 10 9 eqeq12d ⊢ ( Iop = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( ( Iop ∘ Iop ) = Iop ↔ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) )
12 8 11 anbi12d ⊢ ( Iop = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) → ( ( Iop ∈ HrmOp ∧ ( Iop ∘ Iop ) = Iop ) ↔ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ HrmOp ∧ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) ) )
13 idhmop ⊢ Iop ∈ HrmOp
14 hoif ⊢ Iop : ℋ –1-1-onto→ ℋ
15 f1of ⊢ ( Iop : ℋ –1-1-onto→ ℋ → Iop : ℋ ⟶ ℋ )
16 14 15 ax-mp ⊢ Iop : ℋ ⟶ ℋ
17 16 hoid1i ⊢ ( Iop ∘ Iop ) = Iop
18 13 17 pm3.2i ⊢ ( Iop ∈ HrmOp ∧ ( Iop ∘ Iop ) = Iop )
19 7 12 18 elimhyp ⊢ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ HrmOp ∧ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) )
20 19 simpli ⊢ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ HrmOp
21 19 simpri ⊢ ( if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∘ if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ) = if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop )
22 20 21 hmopidmchi ⊢ ran if ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) , 𝑇 , Iop ) ∈ Cℋ
23 2 22 dedth ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) → ran 𝑇 ∈ Cℋ )