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