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 A C
mdslmd.2 B C
mdslmd.3 C C
mdslmd.4 D C
Assertion mdslmd3i A 𝑀 B A B 𝑀 C A C D D A D 𝑀 B C

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 chlej2 D C A C x C D A x D x A
6 5 ex D C A C x C D A x D x A
7 4 1 6 mp3an12 x C D A x D x A
8 7 impcom D A x C x D x A
9 8 ssrind D A x C x D B C x A B C
10 9 adantll A C D D A x C x D B C x A B C
11 10 adantll A 𝑀 B A B 𝑀 C A C D D A x C x D B C x A B C
12 11 adantr A 𝑀 B A B 𝑀 C A C D D A x C x B C x D B C x A B C
13 ssin x B x C x B C
14 inass x A B C = x A B C
15 mdi A C B C x C A 𝑀 B x B x A B = x A B
16 1 15 mp3anl1 B C x C A 𝑀 B x B x A B = x A B
17 2 16 mpanl1 x C A 𝑀 B x B x A B = x A B
18 17 ineq1d x C A 𝑀 B x B x A B C = x A B C
19 14 18 eqtr3id x C A 𝑀 B x B x A B C = x A B C
20 19 adantrlr x C A 𝑀 B A B 𝑀 C x B x A B C = x A B C
21 20 adantrrr x C A 𝑀 B A B 𝑀 C x B x C x A B C = x A B C
22 1 2 chincli A B C
23 mdi A B C C C x C A B 𝑀 C x C x A B C = x A B C
24 22 23 mp3anl1 C C x C A B 𝑀 C x C x A B C = x A B C
25 3 24 mpanl1 x C A B 𝑀 C x C x A B C = x A B C
26 inass A B C = A B C
27 26 oveq2i x A B C = x A B C
28 25 27 eqtrdi x C A B 𝑀 C x C x A B C = x A B C
29 28 adantrll x C A 𝑀 B A B 𝑀 C x C x A B C = x A B C
30 29 adantrrl x C A 𝑀 B A B 𝑀 C x B x C x A B C = x A B C
31 21 30 eqtrd x C A 𝑀 B A B 𝑀 C x B x C x A B C = x A B C
32 31 ancoms A 𝑀 B A B 𝑀 C x B x C x C x A B C = x A B C
33 32 an32s A 𝑀 B A B 𝑀 C x C x B x C x A B C = x A B C
34 13 33 sylan2br A 𝑀 B A B 𝑀 C x C x B C x A B C = x A B C
35 34 adantllr A 𝑀 B A B 𝑀 C A C D D A x C x B C x A B C = x A B C
36 inass A C B C = A C B C
37 in12 C B C = B C C
38 inidm C C = C
39 38 ineq2i B C C = B C
40 37 39 eqtri C B C = B C
41 40 ineq2i A C B C = A B C
42 36 41 eqtr2i A B C = A C B C
43 ssrin A C D A C B C D B C
44 42 43 eqsstrid A C D A B C D B C
45 ssrin D A D B C A B C
46 44 45 anim12i A C D D A A B C D B C D B C A B C
47 eqss A B C = D B C A B C D B C D B C A B C
48 46 47 sylibr A C D D A A B C = D B C
49 48 oveq2d A C D D A x A B C = x D B C
50 49 ad3antlr A 𝑀 B A B 𝑀 C A C D D A x C x B C x A B C = x D B C
51 35 50 eqtrd A 𝑀 B A B 𝑀 C A C D D A x C x B C x A B C = x D B C
52 12 51 sseqtrd A 𝑀 B A B 𝑀 C A C D D A x C x B C x D B C x D B C
53 52 ex A 𝑀 B A B 𝑀 C A C D D A x C x B C x D B C x D B C
54 53 ralrimiva A 𝑀 B A B 𝑀 C A C D D A x C x B C x D B C x D B C
55 2 3 chincli B C C
56 mdbr2 D C B C C D 𝑀 B C x C x B C x D B C x D B C
57 4 55 56 mp2an D 𝑀 B C x C x B C x D B C x D B C
58 54 57 sylibr A 𝑀 B A B 𝑀 C A C D D A D 𝑀 B C