Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Properties of Hilbert subspaces
Commutes relation for Hilbert lattice elements
cmbri
Metamath Proof Explorer
Description: Binary relation expressing the commutes relation. Definition of
commutes in Kalmbach p. 20. (Contributed by NM , 6-Aug-2004)
(New usage is discouraged.)
Ref
Expression
Hypotheses
pjoml2.1
⊢ 𝐴 ∈ C ℋ
pjoml2.2
⊢ 𝐵 ∈ C ℋ
Assertion
cmbri
⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
Proof
Step
Hyp
Ref
Expression
1
pjoml2.1
⊢ 𝐴 ∈ C ℋ
2
pjoml2.2
⊢ 𝐵 ∈ C ℋ
3
cmbr
⊢ ( ( 𝐴 ∈ C ℋ ∧ 𝐵 ∈ C ℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
4
1 2 3
mp2an
⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )