Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Properties of Hilbert subspaces
Foulis-Holland theorem
cm2mi
Metamath Proof Explorer
Description: A lattice element that commutes with two others also commutes with their
meet. Theorem 4.2 of Beran p. 49. (Contributed by NM , 11-May-2009)
(New usage is discouraged.)
Ref
Expression
Hypotheses
fh1.1
⊢ 𝐴 ∈ C ℋ
fh1.2
⊢ 𝐵 ∈ C ℋ
fh1.3
⊢ 𝐶 ∈ C ℋ
fh1.4
⊢ 𝐴 𝐶ℋ 𝐵
fh1.5
⊢ 𝐴 𝐶ℋ 𝐶
Assertion
cm2mi
⊢ 𝐴 𝐶ℋ ( 𝐵 ∩ 𝐶 )
Proof
Step
Hyp
Ref
Expression
1
fh1.1
⊢ 𝐴 ∈ C ℋ
2
fh1.2
⊢ 𝐵 ∈ C ℋ
3
fh1.3
⊢ 𝐶 ∈ C ℋ
4
fh1.4
⊢ 𝐴 𝐶ℋ 𝐵
5
fh1.5
⊢ 𝐴 𝐶ℋ 𝐶
6
2
choccli
⊢ ( ⊥ ‘ 𝐵 ) ∈ C ℋ
7
3
choccli
⊢ ( ⊥ ‘ 𝐶 ) ∈ C ℋ
8
1 2 4
cmcm2ii
⊢ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 )
9
1 3 5
cmcm2ii
⊢ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐶 )
10
1 6 7 8 9
cm2ji
⊢ 𝐴 𝐶ℋ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐶 ) )
11
2 3
chdmm1i
⊢ ( ⊥ ‘ ( 𝐵 ∩ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐶 ) )
12
10 11
breqtrri
⊢ 𝐴 𝐶ℋ ( ⊥ ‘ ( 𝐵 ∩ 𝐶 ) )
13
2 3
chincli
⊢ ( 𝐵 ∩ 𝐶 ) ∈ C ℋ
14
1 13
cmcm2i
⊢ ( 𝐴 𝐶ℋ ( 𝐵 ∩ 𝐶 ) ↔ 𝐴 𝐶ℋ ( ⊥ ‘ ( 𝐵 ∩ 𝐶 ) ) )
15
12 14
mpbir
⊢ 𝐴 𝐶ℋ ( 𝐵 ∩ 𝐶 )