Metamath Proof Explorer


Theorem mdslmd3i

Description: Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of MaedaMaeda p. 2. (Contributed by NM, 23-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdslmd.1 𝐴C
mdslmd.2 𝐵C
mdslmd.3 𝐶C
mdslmd.4 𝐷C
Assertion mdslmd3i ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) → 𝐷 𝑀 ( 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 mdslmd.1 𝐴C
2 mdslmd.2 𝐵C
3 mdslmd.3 𝐶C
4 mdslmd.4 𝐷C
5 chlej2 ( ( ( 𝐷C𝐴C𝑥C ) ∧ 𝐷𝐴 ) → ( 𝑥 𝐷 ) ⊆ ( 𝑥 𝐴 ) )
6 5 ex ( ( 𝐷C𝐴C𝑥C ) → ( 𝐷𝐴 → ( 𝑥 𝐷 ) ⊆ ( 𝑥 𝐴 ) ) )
7 4 1 6 mp3an12 ( 𝑥C → ( 𝐷𝐴 → ( 𝑥 𝐷 ) ⊆ ( 𝑥 𝐴 ) ) )
8 7 impcom ( ( 𝐷𝐴𝑥C ) → ( 𝑥 𝐷 ) ⊆ ( 𝑥 𝐴 ) )
9 8 ssrind ( ( 𝐷𝐴𝑥C ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) )
10 9 adantll ( ( ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ∧ 𝑥C ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) )
11 10 adantll ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) ∧ 𝑥C ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) )
12 11 adantr ( ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) ∧ 𝑥C ) ∧ 𝑥 ⊆ ( 𝐵𝐶 ) ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) )
13 ssin ( ( 𝑥𝐵𝑥𝐶 ) ↔ 𝑥 ⊆ ( 𝐵𝐶 ) )
14 inass ( ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) )
15 mdi ( ( ( 𝐴C𝐵C𝑥C ) ∧ ( 𝐴 𝑀 𝐵𝑥𝐵 ) ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) )
16 1 15 mp3anl1 ( ( ( 𝐵C𝑥C ) ∧ ( 𝐴 𝑀 𝐵𝑥𝐵 ) ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) )
17 2 16 mpanl1 ( ( 𝑥C ∧ ( 𝐴 𝑀 𝐵𝑥𝐵 ) ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) )
18 17 ineq1d ( ( 𝑥C ∧ ( 𝐴 𝑀 𝐵𝑥𝐵 ) ) → ( ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) )
19 14 18 eqtr3id ( ( 𝑥C ∧ ( 𝐴 𝑀 𝐵𝑥𝐵 ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) )
20 19 adantrlr ( ( 𝑥C ∧ ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ 𝑥𝐵 ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) )
21 20 adantrrr ( ( 𝑥C ∧ ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( 𝑥𝐵𝑥𝐶 ) ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) )
22 1 2 chincli ( 𝐴𝐵 ) ∈ C
23 mdi ( ( ( ( 𝐴𝐵 ) ∈ C𝐶C𝑥C ) ∧ ( ( 𝐴𝐵 ) 𝑀 𝐶𝑥𝐶 ) ) → ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ( ( 𝐴𝐵 ) ∩ 𝐶 ) ) )
24 22 23 mp3anl1 ( ( ( 𝐶C𝑥C ) ∧ ( ( 𝐴𝐵 ) 𝑀 𝐶𝑥𝐶 ) ) → ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ( ( 𝐴𝐵 ) ∩ 𝐶 ) ) )
25 3 24 mpanl1 ( ( 𝑥C ∧ ( ( 𝐴𝐵 ) 𝑀 𝐶𝑥𝐶 ) ) → ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ( ( 𝐴𝐵 ) ∩ 𝐶 ) ) )
26 inass ( ( 𝐴𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∩ ( 𝐵𝐶 ) )
27 26 oveq2i ( 𝑥 ( ( 𝐴𝐵 ) ∩ 𝐶 ) ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) )
28 25 27 eqtrdi ( ( 𝑥C ∧ ( ( 𝐴𝐵 ) 𝑀 𝐶𝑥𝐶 ) ) → ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
29 28 adantrll ( ( 𝑥C ∧ ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ 𝑥𝐶 ) ) → ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
30 29 adantrrl ( ( 𝑥C ∧ ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( 𝑥𝐵𝑥𝐶 ) ) ) → ( ( 𝑥 ( 𝐴𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
31 21 30 eqtrd ( ( 𝑥C ∧ ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( 𝑥𝐵𝑥𝐶 ) ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
32 31 ancoms ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( 𝑥𝐵𝑥𝐶 ) ) ∧ 𝑥C ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
33 32 an32s ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ 𝑥C ) ∧ ( 𝑥𝐵𝑥𝐶 ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
34 13 33 sylan2br ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ 𝑥C ) ∧ 𝑥 ⊆ ( 𝐵𝐶 ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
35 34 adantllr ( ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) ∧ 𝑥C ) ∧ 𝑥 ⊆ ( 𝐵𝐶 ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
36 inass ( ( 𝐴𝐶 ) ∩ ( 𝐵𝐶 ) ) = ( 𝐴 ∩ ( 𝐶 ∩ ( 𝐵𝐶 ) ) )
37 in12 ( 𝐶 ∩ ( 𝐵𝐶 ) ) = ( 𝐵 ∩ ( 𝐶𝐶 ) )
38 inidm ( 𝐶𝐶 ) = 𝐶
39 38 ineq2i ( 𝐵 ∩ ( 𝐶𝐶 ) ) = ( 𝐵𝐶 )
40 37 39 eqtri ( 𝐶 ∩ ( 𝐵𝐶 ) ) = ( 𝐵𝐶 )
41 40 ineq2i ( 𝐴 ∩ ( 𝐶 ∩ ( 𝐵𝐶 ) ) ) = ( 𝐴 ∩ ( 𝐵𝐶 ) )
42 36 41 eqtr2i ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐶 ) ∩ ( 𝐵𝐶 ) )
43 ssrin ( ( 𝐴𝐶 ) ⊆ 𝐷 → ( ( 𝐴𝐶 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵𝐶 ) ) )
44 42 43 eqsstrid ( ( 𝐴𝐶 ) ⊆ 𝐷 → ( 𝐴 ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵𝐶 ) ) )
45 ssrin ( 𝐷𝐴 → ( 𝐷 ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵𝐶 ) ) )
46 44 45 anim12i ( ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) → ( ( 𝐴 ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵𝐶 ) ) ∧ ( 𝐷 ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
47 eqss ( ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ( 𝐷 ∩ ( 𝐵𝐶 ) ) ↔ ( ( 𝐴 ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵𝐶 ) ) ∧ ( 𝐷 ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) )
48 46 47 sylibr ( ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) → ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ( 𝐷 ∩ ( 𝐵𝐶 ) ) )
49 48 oveq2d ( ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) → ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) = ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) )
50 49 ad3antlr ( ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) ∧ 𝑥C ) ∧ 𝑥 ⊆ ( 𝐵𝐶 ) ) → ( 𝑥 ( 𝐴 ∩ ( 𝐵𝐶 ) ) ) = ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) )
51 35 50 eqtrd ( ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) ∧ 𝑥C ) ∧ 𝑥 ⊆ ( 𝐵𝐶 ) ) → ( ( 𝑥 𝐴 ) ∩ ( 𝐵𝐶 ) ) = ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) )
52 12 51 sseqtrd ( ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) ∧ 𝑥C ) ∧ 𝑥 ⊆ ( 𝐵𝐶 ) ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) )
53 52 ex ( ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) ∧ 𝑥C ) → ( 𝑥 ⊆ ( 𝐵𝐶 ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) ) )
54 53 ralrimiva ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) → ∀ 𝑥C ( 𝑥 ⊆ ( 𝐵𝐶 ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) ) )
55 2 3 chincli ( 𝐵𝐶 ) ∈ C
56 mdbr2 ( ( 𝐷C ∧ ( 𝐵𝐶 ) ∈ C ) → ( 𝐷 𝑀 ( 𝐵𝐶 ) ↔ ∀ 𝑥C ( 𝑥 ⊆ ( 𝐵𝐶 ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) ) ) )
57 4 55 56 mp2an ( 𝐷 𝑀 ( 𝐵𝐶 ) ↔ ∀ 𝑥C ( 𝑥 ⊆ ( 𝐵𝐶 ) → ( ( 𝑥 𝐷 ) ∩ ( 𝐵𝐶 ) ) ⊆ ( 𝑥 ( 𝐷 ∩ ( 𝐵𝐶 ) ) ) ) )
58 54 57 sylibr ( ( ( 𝐴 𝑀 𝐵 ∧ ( 𝐴𝐵 ) 𝑀 𝐶 ) ∧ ( ( 𝐴𝐶 ) ⊆ 𝐷𝐷𝐴 ) ) → 𝐷 𝑀 ( 𝐵𝐶 ) )