This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjadji

Description: A projection is self-adjoint. Property (i) of Beran p. 109. (Contributed by NM, 6-Oct-2000) (New usage is discouraged.)

Ref Expression
Hypothesis pjadjt.1 ⊢ H ∈ C ℋ
Assertion pjadji ⊢ A ∈ ℋ ∧ B ∈ ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih B = A ⋅ ih proj ℎ ⁡ H ⁡ B

Proof

Step Hyp Ref Expression
1 pjadjt.1 ⊢ H ∈ C ℋ
2 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ
3 2 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ H ⁡ A ⋅ ih B = proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B
4 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih proj ℎ ⁡ H ⁡ B = if A ∈ ℋ A 0 ℎ ⋅ ih proj ℎ ⁡ H ⁡ B
5 3 4 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ H ⁡ A ⋅ ih B = A ⋅ ih proj ℎ ⁡ H ⁡ B ↔ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih proj ℎ ⁡ H ⁡ B
6 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B = proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
7 fveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → proj ℎ ⁡ H ⁡ B = proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
8 7 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih proj ℎ ⁡ H ⁡ B = if A ∈ ℋ A 0 ℎ ⋅ ih proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
9 6 8 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih proj ℎ ⁡ H ⁡ B ↔ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ ⋅ ih proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
10 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
11 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
12 1 10 11 pjadjii ⊢ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ ⋅ ih proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
13 5 9 12 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih B = A ⋅ ih proj ℎ ⁡ H ⁡ B