Metamath Proof Explorer

Theorem mdsldmd1i

Description: Preservation of the dual modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdslmd.1 ⊢ A ∈ C ℋ
mdslmd.2 ⊢ B ∈ C ℋ
mdslmd.3 ⊢ C ∈ C ℋ
mdslmd.4 ⊢ D ∈ C ℋ
Assertion mdsldmd1i ⊢ A 𝑀 ℋ B ∧ B 𝑀 ℋ * A ∧ A ⊆ C ∩ D ∧ C ∨ ℋ D ⊆ A ∨ ℋ B → C 𝑀 ℋ * D ↔ C ∩ B 𝑀 ℋ * D ∩ B

Proof

Step Hyp Ref Expression
1 mdslmd.1 ⊢ A ∈ C ℋ
2 mdslmd.2 ⊢ B ∈ C ℋ
3 mdslmd.3 ⊢ C ∈ C ℋ
4 mdslmd.4 ⊢ D ∈ C ℋ
5 mddmd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ B ↔ ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B
6 1 2 5 mp2an ⊢ A 𝑀 ℋ B ↔ ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B
7 dmdmd ⊢ B ∈ C ℋ ∧ A ∈ C ℋ → B 𝑀 ℋ * A ↔ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A
8 2 1 7 mp2an ⊢ B 𝑀 ℋ * A ↔ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A
9 6 8 anbi12ci ⊢ A 𝑀 ℋ B ∧ B 𝑀 ℋ * A ↔ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A ∧ ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B
10 3 4 chincli ⊢ C ∩ D ∈ C ℋ
11 1 10 chsscon3i ⊢ A ⊆ C ∩ D ↔ ⊥ ⁡ C ∩ D ⊆ ⊥ ⁡ A
12 3 4 chdmm1i ⊢ ⊥ ⁡ C ∩ D = ⊥ ⁡ C ∨ ℋ ⊥ ⁡ D
13 12 sseq1i ⊢ ⊥ ⁡ C ∩ D ⊆ ⊥ ⁡ A ↔ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ D ⊆ ⊥ ⁡ A
14 11 13 bitri ⊢ A ⊆ C ∩ D ↔ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ D ⊆ ⊥ ⁡ A
15 3 4 chjcli ⊢ C ∨ ℋ D ∈ C ℋ
16 1 2 chjcli ⊢ A ∨ ℋ B ∈ C ℋ
17 15 16 chsscon3i ⊢ C ∨ ℋ D ⊆ A ∨ ℋ B ↔ ⊥ ⁡ A ∨ ℋ B ⊆ ⊥ ⁡ C ∨ ℋ D
18 1 2 chdmj1i ⊢ ⊥ ⁡ A ∨ ℋ B = ⊥ ⁡ A ∩ ⊥ ⁡ B
19 incom ⊢ ⊥ ⁡ A ∩ ⊥ ⁡ B = ⊥ ⁡ B ∩ ⊥ ⁡ A
20 18 19 eqtri ⊢ ⊥ ⁡ A ∨ ℋ B = ⊥ ⁡ B ∩ ⊥ ⁡ A
21 3 4 chdmj1i ⊢ ⊥ ⁡ C ∨ ℋ D = ⊥ ⁡ C ∩ ⊥ ⁡ D
22 20 21 sseq12i ⊢ ⊥ ⁡ A ∨ ℋ B ⊆ ⊥ ⁡ C ∨ ℋ D ↔ ⊥ ⁡ B ∩ ⊥ ⁡ A ⊆ ⊥ ⁡ C ∩ ⊥ ⁡ D
23 17 22 bitri ⊢ C ∨ ℋ D ⊆ A ∨ ℋ B ↔ ⊥ ⁡ B ∩ ⊥ ⁡ A ⊆ ⊥ ⁡ C ∩ ⊥ ⁡ D
24 14 23 anbi12ci ⊢ A ⊆ C ∩ D ∧ C ∨ ℋ D ⊆ A ∨ ℋ B ↔ ⊥ ⁡ B ∩ ⊥ ⁡ A ⊆ ⊥ ⁡ C ∩ ⊥ ⁡ D ∧ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ D ⊆ ⊥ ⁡ A
25 2 choccli ⊢ ⊥ ⁡ B ∈ C ℋ
26 1 choccli ⊢ ⊥ ⁡ A ∈ C ℋ
27 3 choccli ⊢ ⊥ ⁡ C ∈ C ℋ
28 4 choccli ⊢ ⊥ ⁡ D ∈ C ℋ
29 25 26 27 28 mdslmd2i ⊢ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A ∧ ⊥ ⁡ A 𝑀 ℋ * ⊥ ⁡ B ∧ ⊥ ⁡ B ∩ ⊥ ⁡ A ⊆ ⊥ ⁡ C ∩ ⊥ ⁡ D ∧ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ D ⊆ ⊥ ⁡ A → ⊥ ⁡ C 𝑀 ℋ ⊥ ⁡ D ↔ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ D ∨ ℋ ⊥ ⁡ B
30 9 24 29 syl2anb ⊢ A 𝑀 ℋ B ∧ B 𝑀 ℋ * A ∧ A ⊆ C ∩ D ∧ C ∨ ℋ D ⊆ A ∨ ℋ B → ⊥ ⁡ C 𝑀 ℋ ⊥ ⁡ D ↔ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ D ∨ ℋ ⊥ ⁡ B
31 dmdmd ⊢ C ∈ C ℋ ∧ D ∈ C ℋ → C 𝑀 ℋ * D ↔ ⊥ ⁡ C 𝑀 ℋ ⊥ ⁡ D
32 3 4 31 mp2an ⊢ C 𝑀 ℋ * D ↔ ⊥ ⁡ C 𝑀 ℋ ⊥ ⁡ D
33 3 2 chincli ⊢ C ∩ B ∈ C ℋ
34 4 2 chincli ⊢ D ∩ B ∈ C ℋ
35 dmdmd ⊢ C ∩ B ∈ C ℋ ∧ D ∩ B ∈ C ℋ → C ∩ B 𝑀 ℋ * D ∩ B ↔ ⊥ ⁡ C ∩ B 𝑀 ℋ ⊥ ⁡ D ∩ B
36 33 34 35 mp2an ⊢ C ∩ B 𝑀 ℋ * D ∩ B ↔ ⊥ ⁡ C ∩ B 𝑀 ℋ ⊥ ⁡ D ∩ B
37 3 2 chdmm1i ⊢ ⊥ ⁡ C ∩ B = ⊥ ⁡ C ∨ ℋ ⊥ ⁡ B
38 4 2 chdmm1i ⊢ ⊥ ⁡ D ∩ B = ⊥ ⁡ D ∨ ℋ ⊥ ⁡ B
39 37 38 breq12i ⊢ ⊥ ⁡ C ∩ B 𝑀 ℋ ⊥ ⁡ D ∩ B ↔ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ D ∨ ℋ ⊥ ⁡ B
40 36 39 bitri ⊢ C ∩ B 𝑀 ℋ * D ∩ B ↔ ⊥ ⁡ C ∨ ℋ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ D ∨ ℋ ⊥ ⁡ B
41 30 32 40 3bitr4g ⊢ A 𝑀 ℋ B ∧ B 𝑀 ℋ * A ∧ A ⊆ C ∩ D ∧ C ∨ ℋ D ⊆ A ∨ ℋ B → C 𝑀 ℋ * D ↔ C ∩ B 𝑀 ℋ * D ∩ B