Metamath Proof Explorer

Theorem hmopidmpj

Description: An idempotent Hermitian operator is a projection operator. Theorem 26.4 of Halmos p. 44. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopidmpj ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) → 𝑇 = ( projℎ ‘ ran 𝑇 ) )

Proof

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