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 e. CH
	mdsl.2	\|- B e. CH
Assertion	mdsl1i	\|- ( A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) <-> A MH B )

Proof

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

Metamath Proof Explorer

Theorem mdsl1i

Proof