Metamath Proof Explorer

Theorem cmbr3i

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 cmcmi ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴 )
4 2 1 cmbr2i ⊢ ( 𝐵 𝐶ℋ 𝐴 ↔ 𝐵 = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) )
5 3 4 bitri ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐵 = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) )
6 ineq2 ⊢ ( 𝐵 = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∩ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ) )
7 inass ⊢ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐴 ) ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝐴 ∩ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) )
8 2 1 chjcomi ⊢ ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 )
9 8 ineq2i ⊢ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) )
10 1 2 chabs2i ⊢ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴
11 9 10 eqtri ⊢ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = 𝐴
12 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
13 2 12 chjcomi ⊢ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
14 11 13 ineq12i ⊢ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐴 ) ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
15 7 14 eqtr3i ⊢ ( 𝐴 ∩ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
16 6 15 eqtr2di ⊢ ( 𝐵 = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) )
17 5 16 sylbi ⊢ ( 𝐴 𝐶ℋ 𝐵 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) )
18 inss1 ⊢ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ⊆ 𝐴
19 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
20 1 19 chincli ⊢ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
21 20 1 pjoml2i ⊢ ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ⊆ 𝐴 → ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ) = 𝐴 )
22 18 21 ax-mp ⊢ ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ) = 𝐴
23 20 choccli ⊢ ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∈ Cℋ
24 23 1 chincli ⊢ ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ∈ Cℋ
25 20 24 chjcomi ⊢ ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ) = ( ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )
26 22 25 eqtr3i ⊢ 𝐴 = ( ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )
27 1 2 chdmm3i ⊢ ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
28 27 ineq2i ⊢ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
29 incom ⊢ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 )
30 28 29 eqtr3i ⊢ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 )
31 30 eqeq1i ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) ↔ ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) )
32 oveq1 ⊢ ( ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) → ( ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
33 31 32 sylbi ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) → ( ( ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ∩ 𝐴 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
34 26 33 syl5eq ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) → 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
35 1 2 cmbri ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
36 34 35 sylibr ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) → 𝐴 𝐶ℋ 𝐵 )
37 17 36 impbii ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) )