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 ⊢ A ∈ C ℋ
mdsym.2 ⊢ B ∈ C ℋ
Assertion mdsymi ⊢ A 𝑀 ℋ B ↔ B 𝑀 ℋ A

Proof

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