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

Metamath Proof Explorer

Theorem cmcm2i

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. (Contributed by NM, 4-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ 𝐴 ∈ Cℋ
pjoml2.2 ⊢ 𝐵 ∈ Cℋ
Assertion cmcm2i ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
4 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
5 1 4 chincli ⊢ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
6 3 5 chjcomi ⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )
7 2 pjococi ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵
8 7 ineq2i ⊢ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ 𝐵 )
9 8 oveq2i ⊢ ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )
10 6 9 eqtr4i ⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
11 10 eqeq2i ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ↔ 𝐴 = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
12 1 2 cmbri ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
13 1 4 cmbri ⊢ ( 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) ↔ 𝐴 = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
14 11 12 13 3bitr4i ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) )