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

Metamath Proof Explorer

Theorem mdslj2i

Description: Meet preservation of the reverse mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdslle1.1 ⊢ 𝐴 ∈ Cℋ
mdslle1.2 ⊢ 𝐵 ∈ Cℋ
mdslle1.3 ⊢ 𝐶 ∈ Cℋ
mdslle1.4 ⊢ 𝐷 ∈ Cℋ
Assertion mdslj2i ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 mdslle1.1 ⊢ 𝐴 ∈ Cℋ
2 mdslle1.2 ⊢ 𝐵 ∈ Cℋ
3 mdslle1.3 ⊢ 𝐶 ∈ Cℋ
4 mdslle1.4 ⊢ 𝐷 ∈ Cℋ
5 3 4 1 lejdiri ⊢ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) )
6 5 a1i ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
7 ssin ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) )
8 7 bicomi ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) )
9 3 4 2 chlubi ⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 )
10 9 bicomi ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ↔ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) )
11 8 10 anbi12i ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) )
12 simpr ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐵 𝑀ℋ* 𝐴 )
13 1 3 chub2i ⊢ 𝐴 ⊆ ( 𝐶 ∨ℋ 𝐴 )
14 1 4 chub2i ⊢ 𝐴 ⊆ ( 𝐷 ∨ℋ 𝐴 )
15 13 14 ssini ⊢ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) )
16 15 a1i ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) → 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
17 3 2 1 chlej1i ⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐵 ∨ℋ 𝐴 ) )
18 2 1 chjcomi ⊢ ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 )
19 17 18 sseqtrdi ⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
20 ssinss1 ⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
21 19 20 syl ⊢ ( 𝐶 ⊆ 𝐵 → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
22 21 adantr ⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
23 3 1 chjcli ⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
24 4 1 chjcli ⊢ ( 𝐷 ∨ℋ 𝐴 ) ∈ Cℋ
25 23 24 chincli ⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∈ Cℋ
26 1 2 25 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∈ Cℋ )
27 dmdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
28 26 27 mpan ⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
29 12 16 22 28 syl3an ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
30 inss1 ⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐶 ∨ℋ 𝐴 )
31 ssrin ⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐶 ∨ℋ 𝐴 ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
32 30 31 ax-mp ⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 )
33 simpl ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
34 simpl ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
35 simpl ⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) → 𝐶 ⊆ 𝐵 )
36 1 2 3 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
37 mdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
38 36 37 mpan ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
39 33 34 35 38 syl3an ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
40 32 39 sseqtrid ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ 𝐶 )
41 inss2 ⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐷 ∨ℋ 𝐴 )
42 ssrin ⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐷 ∨ℋ 𝐴 ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
43 41 42 ax-mp ⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 )
44 simpr ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 )
45 simpr ⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) → 𝐷 ⊆ 𝐵 )
46 1 2 4 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
47 mdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
48 46 47 mpan ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
49 33 44 45 48 syl3an ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
50 43 49 sseqtrid ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ 𝐷 )
51 40 50 ssind ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) )
52 25 2 chincli ⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∈ Cℋ
53 3 4 chincli ⊢ ( 𝐶 ∩ 𝐷 ) ∈ Cℋ
54 52 53 1 chlej1i ⊢ ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
55 51 54 syl ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
56 29 55 eqsstrrd ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
57 56 3expb ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
58 11 57 sylan2b ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
59 6 58 eqssd ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )