This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdslmd2i

Description: Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2 (join version). (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 mdslmd2i ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ ( 𝐷 ∨ℋ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 mdslmd.1 ⊢ 𝐴 ∈ Cℋ
2 mdslmd.2 ⊢ 𝐵 ∈ Cℋ
3 mdslmd.3 ⊢ 𝐶 ∈ Cℋ
4 mdslmd.4 ⊢ 𝐷 ∈ Cℋ
5 3 4 chjcli ⊢ ( 𝐶 ∨ℋ 𝐷 ) ∈ Cℋ
6 5 2 1 chlej1i ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → ( ( 𝐶 ∨ℋ 𝐷 ) ∨ℋ 𝐴 ) ⊆ ( 𝐵 ∨ℋ 𝐴 ) )
7 3 4 1 chjjdiri ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) )
8 2 1 chjcomi ⊢ ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 )
9 6 7 8 3sstr3g ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
10 9 adantl ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
11 1 3 chub2i ⊢ 𝐴 ⊆ ( 𝐶 ∨ℋ 𝐴 )
12 1 4 chub2i ⊢ 𝐴 ⊆ ( 𝐷 ∨ℋ 𝐴 )
13 11 12 ssini ⊢ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) )
14 10 13 jctil ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
15 3 1 chjcli ⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
16 4 1 chjcli ⊢ ( 𝐷 ∨ℋ 𝐴 ) ∈ Cℋ
17 1 2 15 16 mdslmd1i ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ ( 𝐷 ∨ℋ 𝐴 ) ↔ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
18 14 17 sylan2 ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ ( 𝐷 ∨ℋ 𝐴 ) ↔ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
19 id ⊢ ( 𝐴 𝑀ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵 )
20 inss1 ⊢ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐶
21 sstr ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
22 20 21 mpan2 ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
23 3 4 chub1i ⊢ 𝐶 ⊆ ( 𝐶 ∨ℋ 𝐷 )
24 sstr ⊢ ( ( 𝐶 ⊆ ( 𝐶 ∨ℋ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → 𝐶 ⊆ 𝐵 )
25 23 24 mpan ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → 𝐶 ⊆ 𝐵 )
26 1 2 3 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
27 mdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
28 26 27 mpan ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
29 19 22 25 28 syl3an ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
30 inss2 ⊢ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐷
31 sstr ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 )
32 30 31 mpan2 ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 )
33 4 3 chub2i ⊢ 𝐷 ⊆ ( 𝐶 ∨ℋ 𝐷 )
34 sstr ⊢ ( ( 𝐷 ⊆ ( 𝐶 ∨ℋ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → 𝐷 ⊆ 𝐵 )
35 33 34 mpan ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → 𝐷 ⊆ 𝐵 )
36 1 2 4 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
37 mdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
38 36 37 mpan ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
39 19 32 35 38 syl3an ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
40 29 39 breq12d ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ↔ 𝐶 𝑀ℋ 𝐷 ) )
41 40 3expb ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ↔ 𝐶 𝑀ℋ 𝐷 ) )
42 41 adantlr ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ↔ 𝐶 𝑀ℋ 𝐷 ) )
43 18 42 bitr2d ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ ( 𝐷 ∨ℋ 𝐴 ) ) )