Metamath Proof Explorer


Theorem mdsl1i

Description: If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdsl.1 A C
mdsl.2 B C
Assertion mdsl1i x C A B x x A B x B x A B = x A B A 𝑀 B

Proof

Step Hyp Ref Expression
1 mdsl.1 A C
2 mdsl.2 B C
3 sseq2 x = y A B A B x A B y A B
4 sseq1 x = y A B x A B y A B A B
5 3 4 anbi12d x = y A B A B x x A B A B y A B y A B A B
6 sseq1 x = y A B x B y A B B
7 oveq1 x = y A B x A = y A B A
8 7 ineq1d x = y A B x A B = y A B A B
9 oveq1 x = y A B x A B = y A B A B
10 8 9 eqeq12d x = y A B x A B = x A B y A B A B = y A B A B
11 6 10 imbi12d x = y A B x B x A B = x A B y A B B y A B A B = y A B A B
12 5 11 imbi12d x = y A B A B x x A B x B x A B = x A B A B y A B y A B A B y A B B y A B A B = y A B A B
13 12 rspccv x C A B x x A B x B x A B = x A B y A B C A B y A B y A B A B y A B B y A B A B = y A B A B
14 impexp y A B C A B y A B y A B A B y A B B y A B A B = y A B A B y A B C A B y A B y A B A B y A B B y A B A B = y A B A B
15 impexp y A B C A B y A B y A B A B y A B B y A B A B = y A B A B y A B C A B y A B y A B A B y A B B y A B A B = y A B A B
16 14 15 bitr2i y A B C A B y A B y A B A B y A B B y A B A B = y A B A B y A B C A B y A B y A B A B y A B B y A B A B = y A B A B
17 inss2 A B B
18 1 2 chincli A B C
19 chlub y C A B C B C y B A B B y A B B
20 18 2 19 mp3an23 y C y B A B B y A B B
21 20 biimpd y C y B A B B y A B B
22 17 21 mpan2i y C y B y A B B
23 2 1 chub2i B A B
24 sstr y A B B B A B y A B A B
25 23 24 mpan2 y A B B y A B A B
26 22 25 syl6 y C y B y A B A B
27 chub2 A B C y C A B y A B
28 18 27 mpan y C A B y A B
29 26 28 jctild y C y B A B y A B y A B A B
30 chjcl y C A B C y A B C
31 18 30 mpan2 y C y A B C
32 29 31 jctild y C y B y A B C A B y A B y A B A B
33 32 22 jcad y C y B y A B C A B y A B y A B A B y A B B
34 chjass y C A B C A C y A B A = y A B A
35 18 1 34 mp3an23 y C y A B A = y A B A
36 18 1 chjcomi A B A = A A B
37 1 2 chabs1i A A B = A
38 36 37 eqtri A B A = A
39 38 oveq2i y A B A = y A
40 35 39 eqtrdi y C y A B A = y A
41 40 ineq1d y C y A B A B = y A B
42 chjass y C A B C A B C y A B A B = y A B A B
43 18 18 42 mp3an23 y C y A B A B = y A B A B
44 18 chjidmi A B A B = A B
45 44 oveq2i y A B A B = y A B
46 43 45 eqtrdi y C y A B A B = y A B
47 41 46 eqeq12d y C y A B A B = y A B A B y A B = y A B
48 47 biimpd y C y A B A B = y A B A B y A B = y A B
49 33 48 imim12d y C y A B C A B y A B y A B A B y A B B y A B A B = y A B A B y B y A B = y A B
50 16 49 syl5bi y C y A B C A B y A B y A B A B y A B B y A B A B = y A B A B y B y A B = y A B
51 13 50 syl5com x C A B x x A B x B x A B = x A B y C y B y A B = y A B
52 51 ralrimiv x C A B x x A B x B x A B = x A B y C y B y A B = y A B
53 mdbr A C B C A 𝑀 B y C y B y A B = y A B
54 1 2 53 mp2an A 𝑀 B y C y B y A B = y A B
55 52 54 sylibr x C A B x x A B x B x A B = x A B A 𝑀 B
56 mdbr A C B C A 𝑀 B x C x B x A B = x A B
57 1 2 56 mp2an A 𝑀 B x C x B x A B = x A B
58 ax-1 x B x A B = x A B A B x x A B x B x A B = x A B
59 58 ralimi x C x B x A B = x A B x C A B x x A B x B x A B = x A B
60 57 59 sylbi A 𝑀 B x C A B x x A B x B x A B = x A B
61 55 60 impbii x C A B x x A B x B x A B = x A B A 𝑀 B