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

Metamath Proof Explorer

Theorem cmbr2i

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 cmcm4i ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ ( ⊥ ‘ 𝐵 ) )
4 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
5 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
6 4 5 cmbri ⊢ ( ( ⊥ ‘ 𝐴 ) 𝐶ℋ ( ⊥ ‘ 𝐵 ) ↔ ( ⊥ ‘ 𝐴 ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
7 eqcom ⊢ ( 𝐴 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = 𝐴 )
8 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
9 1 5 chjcli ⊢ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
10 8 9 chincli ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∈ Cℋ
11 10 1 chcon3i ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = 𝐴 ↔ ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) )
12 8 9 chdmm1i ⊢ ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) )
13 1 2 chdmj1i ⊢ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) )
14 1 5 chdmj1i ⊢ ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
15 13 14 oveq12i ⊢ ( ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
16 12 15 eqtri ⊢ ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
17 16 eqeq2i ⊢ ( ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ( ⊥ ‘ 𝐴 ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
18 7 11 17 3bitrri ⊢ ( ( ⊥ ‘ 𝐴 ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ 𝐴 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) )
19 3 6 18 3bitri ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) )