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 ( 𝐴 𝐶 𝐵𝐴 𝐶 ( ⊥ ‘ 𝐵 ) )