Metamath Proof Explorer

Theorem cmcmlem

Description: Commutation is symmetric. Theorem 3.4 of Beran p. 45. (Contributed by NM, 3-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ 𝐴 ∈ Cℋ
pjoml2.2 ⊢ 𝐵 ∈ Cℋ
Assertion cmcmlem ( 𝐴 𝐶ℋ 𝐵 → 𝐵 𝐶ℋ 𝐴 )

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
4 2 3 chub2i ⊢ 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
5 sseqin2 ⊢ ( 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝐵 ) = 𝐵 )
6 4 5 mpbi ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝐵 ) = 𝐵
7 6 ineq2i ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝐵 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 )
8 inass ⊢ ( ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝐵 ) )
9 1 2 chdmm1i ⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) )
10 9 ineq1i ⊢ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 )
11 7 8 10 3eqtr4ri ⊢ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) = ( ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ∩ 𝐵 )
12 1 2 chdmj4i ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ 𝐵 )
13 1 2 chdmj2i ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) )
14 12 13 oveq12i ⊢ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )
15 14 eqeq2i ⊢ ( 𝐴 = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ) ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
16 15 biimpri ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → 𝐴 = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
17 16 fveq2d ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ) ) )
18 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
19 3 18 chjcli ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
20 3 2 chjcli ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ∈ Cℋ
21 19 20 chdmj4i ⊢ ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
22 17 21 eqtr2di ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ⊥ ‘ 𝐴 ) )
23 22 ineq1d ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) )
24 11 23 syl5eq ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) )
25 24 oveq2d ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
26 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
27 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
28 27 2 pjoml2i ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) ) = 𝐵 )
29 26 28 ax-mp ⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) ) = 𝐵
30 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
31 incom ⊢ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) )
32 30 31 oveq12i ⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) )
33 25 29 32 3eqtr3g ⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → 𝐵 = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ) )
34 1 2 cmbri ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
35 2 1 cmbri ⊢ ( 𝐵 𝐶ℋ 𝐴 ↔ 𝐵 = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ) )
36 33 34 35 3imtr4i ⊢ ( 𝐴 𝐶ℋ 𝐵 → 𝐵 𝐶ℋ 𝐴 )