Metamath Proof Explorer

Theorem mdsymi

Description: M-symmetry of the Hilbert lattice. Lemma 5 of Maeda p. 168. (Contributed by NM, 3-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsym.1 ⊢ 𝐴 ∈ Cℋ
mdsym.2 ⊢ 𝐵 ∈ Cℋ
Assertion mdsymi ( 𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴 )

Proof

Step Hyp Ref Expression
1 mdsym.1 ⊢ 𝐴 ∈ Cℋ
2 mdsym.2 ⊢ 𝐵 ∈ Cℋ
3 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
4 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
5 eqid ⊢ ( ( ⊥ ‘ 𝐵 ) ∨ℋ 𝑥 ) = ( ( ⊥ ‘ 𝐵 ) ∨ℋ 𝑥 )
6 3 4 5 mdsymlem8 ⊢ ( ( ( ⊥ ‘ 𝐵 ) ≠ 0ℋ ∧ ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ) → ( ( ⊥ ‘ 𝐴 ) 𝑀ℋ* ( ⊥ ‘ 𝐵 ) ↔ ( ⊥ ‘ 𝐵 ) 𝑀ℋ* ( ⊥ ‘ 𝐴 ) ) )
7 mddmd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝑀ℋ* ( ⊥ ‘ 𝐵 ) ) )
8 1 2 7 mp2an ⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝑀ℋ* ( ⊥ ‘ 𝐵 ) )
9 mddmd ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐵 𝑀ℋ 𝐴 ↔ ( ⊥ ‘ 𝐵 ) 𝑀ℋ* ( ⊥ ‘ 𝐴 ) ) )
10 2 1 9 mp2an ⊢ ( 𝐵 𝑀ℋ 𝐴 ↔ ( ⊥ ‘ 𝐵 ) 𝑀ℋ* ( ⊥ ‘ 𝐴 ) )
11 6 8 10 3bitr4g ⊢ ( ( ( ⊥ ‘ 𝐵 ) ≠ 0ℋ ∧ ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴 ) )
12 1 chssii ⊢ 𝐴 ⊆ ℋ
13 fveq2 ⊢ ( ( ⊥ ‘ 𝐵 ) = 0ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = ( ⊥ ‘ 0ℋ ) )
14 2 pjococi ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵
15 choc0 ⊢ ( ⊥ ‘ 0ℋ ) = ℋ
16 13 14 15 3eqtr3g ⊢ ( ( ⊥ ‘ 𝐵 ) = 0ℋ → 𝐵 = ℋ )
17 12 16 sseqtrrid ⊢ ( ( ⊥ ‘ 𝐵 ) = 0ℋ → 𝐴 ⊆ 𝐵 )
18 ssmd1 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 𝑀ℋ 𝐵 )
19 1 2 18 mp3an12 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 𝑀ℋ 𝐵 )
20 ssmd2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 𝑀ℋ 𝐴 )
21 1 2 20 mp3an12 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐵 𝑀ℋ 𝐴 )
22 19 21 jca ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ 𝐴 ) )
23 pm5.1 ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ 𝐴 ) → ( 𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴 ) )
24 17 22 23 3syl ⊢ ( ( ⊥ ‘ 𝐵 ) = 0ℋ → ( 𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴 ) )
25 2 chssii ⊢ 𝐵 ⊆ ℋ
26 fveq2 ⊢ ( ( ⊥ ‘ 𝐴 ) = 0ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = ( ⊥ ‘ 0ℋ ) )
27 1 pjococi ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
28 26 27 15 3eqtr3g ⊢ ( ( ⊥ ‘ 𝐴 ) = 0ℋ → 𝐴 = ℋ )
29 25 28 sseqtrrid ⊢ ( ( ⊥ ‘ 𝐴 ) = 0ℋ → 𝐵 ⊆ 𝐴 )
30 ssmd2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝐵 ⊆ 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
31 2 1 30 mp3an12 ⊢ ( 𝐵 ⊆ 𝐴 → 𝐴 𝑀ℋ 𝐵 )
32 ssmd1 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 𝑀ℋ 𝐴 )
33 2 1 32 mp3an12 ⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 𝑀ℋ 𝐴 )
34 31 33 jca ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ 𝐴 ) )
35 29 34 23 3syl ⊢ ( ( ⊥ ‘ 𝐴 ) = 0ℋ → ( 𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴 ) )
36 11 24 35 pm2.61iine ⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴 )