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 ⊢ 𝐴 ∈ Cℋ
mdslmd.2 ⊢ 𝐵 ∈ Cℋ
mdslmd.3 ⊢ 𝐶 ∈ Cℋ
mdslmd.4 ⊢ 𝐷 ∈ Cℋ
Assertion mdsldmd1i ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 𝑀ℋ* 𝐷 ↔ ( 𝐶 ∩ 𝐵 ) 𝑀ℋ* ( 𝐷 ∩ 𝐵 ) ) )

Proof

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