Theorem mdsl1 10185

Description: If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of [MaedaMaeda] p. 2.

Hypotheses

Ref	Expression
mdsl.1	|- A e. CH
mdsl.2	|- B e. CH

Assertion

Ref	Expression
mdsl1	|- (A.x e. CH (((A i^i B) (_ x /\ x (_ (A vH B)) -> (x (_ B -> ((x vH A) i^i B) = (x vH (A i^i B)))) <-> A MH B)

Distinct variable groups:   x,A   x,B

Proof of Theorem mdsl1

Step	Hyp	Ref	Expression
1		inss2 2227	. . . . . . . . . . . 12 |- (A i^i B) (_ B
2		mdsl.1	. . . . . . . . . . . . . . 15 |- A e. CH
3		mdsl.2	. . . . . . . . . . . . . . 15 |- B e. CH
4	2, 3	chincl 9321	. . . . . . . . . . . . . 14 |- (A i^i B) e. CH
5		chlubt 9370	. . . . . . . . . . . . . 14 |- ((y e. CH /\ (A i^i B) e. CH /\ B e. CH) -> ((y (_ B /\ (A i^i B) (_ B) <-> (y vH (A i^i B)) (_ B))
6	4, 3, 5	mp3an23 906	. . . . . . . . . . . . 13 |- (y e. CH -> ((y (_ B /\ (A i^i B) (_ B) <-> (y vH (A i^i B)) (_ B))
7	6	biimpd 153	. . . . . . . . . . . 12 |- (y e. CH -> ((y (_ B /\ (A i^i B) (_ B) -> (y vH (A i^i B)) (_ B))
8	1, 7	mpan2i 698	. . . . . . . . . . 11 |- (y e. CH -> (y (_ B -> (y vH (A i^i B)) (_ B))
9	3, 2	chub2 9331	. . . . . . . . . . . 12 |- B (_ (A vH B)
10		sstr 2068	. . . . . . . . . . . 12 |- (((y vH (A i^i B)) (_ B /\ B (_ (A vH B)) -> (y vH (A i^i B)) (_ (A vH B))
11	9, 10	mpan2 695	. . . . . . . . . . 11 |- ((y vH (A i^i B)) (_ B -> (y vH (A i^i B)) (_ (A vH B))
12	8, 11	syl6 22	. . . . . . . . . 10 |- (y e. CH -> (y (_ B -> (y vH (A i^i B)) (_ (A vH B)))
13		chub2t 9369	. . . . . . . . . . 11 |- (((A i^i B) e. CH /\ y e. CH) -> (A i^i B) (_ (y vH (A i^i B)))
14	4, 13	mpan 694	. . . . . . . . . 10 |- (y e. CH -> (A i^i B) (_ (y vH (A i^i B)))
15	12, 14	jctild 600	. . . . . . . . 9 |- (y e. CH -> (y (_ B -> ((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B))))
16		chjclt 9267	. . . . . . . . . 10 |- ((y e. CH /\ (A i^i B) e. CH) -> (y vH (A i^i B)) e. CH)
17	4, 16	mpan2 695	. . . . . . . . 9 |- (y e. CH -> (y vH (A i^i B)) e. CH)
18	15, 17	jctild 600	. . . . . . . 8 |- (y e. CH -> (y (_ B -> ((y vH (A i^i B)) e. CH /\ ((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B)))))
19	18, 8	jcad 599	. . . . . . 7 |- (y e. CH -> (y (_ B -> (((y vH (A i^i B)) e. CH /\ ((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B))) /\ (y vH (A i^i B)) (_ B)))
20		chjasst 9394	. . . . . . . . . . . 12 |- ((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)))
21	4, 2, 20	mp3an23 906	. . . . . . . . . . 11 |- (y e. CH -> ((y vH (A i^i B)) vH A) = (y vH ((A i^i B) vH A)))
22	4, 2	chjcom 9329	. . . . . . . . . . . . 13 |- ((A i^i B) vH A) = (A vH (A i^i B))
23	2, 3	chabs1 9379	. . . . . . . . . . . . 13 |- (A vH (A i^i B)) = A
24	22, 23	eqtr 1492	. . . . . . . . . . . 12 |- ((A i^i B) vH A) = A
25	24	opreq2i 3963	. . . . . . . . . . 11 |- (y vH ((A i^i B) vH A)) = (y vH A)
26	21, 25	syl6eq 1520	. . . . . . . . . 10 |- (y e. CH -> ((y vH (A i^i B)) vH A) = (y vH A))
27	26	ineq1d 2212	. . . . . . . . 9 |- (y e. CH -> (((y vH (A i^i B)) vH A) i^i B) = ((y vH A) i^i B))
28		chjasst 9394	. . . . . . . . . . 11 |- ((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))))
29	4, 4, 28	mp3an23 906	. . . . . . . . . 10 |- (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))))
30	4	chjidm 9382	. . . . . . . . . . 11 |- ((A i^i B) vH (A i^i B)) = (A i^i B)
31	30	opreq2i 3963	. . . . . . . . . 10 |- (y vH ((A i^i B) vH (A i^i B))) = (y vH (A i^i B))
32	29, 31	syl6eq 1520	. . . . . . . . 9 |- (y e. CH -> ((y vH (A i^i B)) vH (A i^i B)) = (y vH (A i^i B)))
33	27, 32	eqeq12d 1486	. . . . . . . 8 |- (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))))
34	33	biimpd 153	. . . . . . 7 |- (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))))
35	19, 34	imim12d 29	. . . . . 6 |- (y e. CH -> (((((y vH (A i^i B)) e. CH /\ ((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B))) /\ (y vH (A i^i B)) (_ B) -> (((y vH (A i^i B)) vH A) i^i B) = ((y vH (A i^i B)) vH (A i^i B))) -> (y (_ B -> ((y vH A) i^i B) = (y vH (A i^i B)))))
36		impexp 347	. . . . . . 7 |- (((((y vH (A i^i B)) e. CH /\ ((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B))) /\ (y vH (A i^i B)) (_ 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) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B))) -> ((y vH (A i^i B)) (_ B -> (((y vH (A i^i B)) vH A) i^i B) = ((y vH (A i^i B)) vH (A i^i B)))))
37		impexp 347	. . . . . . 7 |- ((((y vH (A i^i B)) e. CH /\ ((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B))) -> ((y vH (A i^i B)) (_ 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) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B)) -> ((y vH (A i^i B)) (_ B -> (((y vH (A i^i B)) vH A) i^i B) = ((y vH (A i^i B)) vH (A i^i B))))))
38	36, 37	bitr2 174	. . . . . 6 |- (((y vH (A i^i B)) e. CH -> (((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B)) -> ((y vH (A i^i B)) (_ 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) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B))) /\ (y vH (A i^i B)) (_ B) -> (((y vH (A i^i B)) vH A) i^i B) = ((y vH (A i^i B)) vH (A i^i B))))
39	35, 38	syl5ib 206	. . . . 5 |- (y e. CH -> (((y vH (A i^i B)) e. CH -> (((A i^i B) (_ (y vH (A i^i B)) /\ (y vH (A i^i B)) (_ (A vH B)) -> ((y vH (A i^i B)) (_ B -> (((y vH (A i^i B)) vH A) i^i B) = ((y vH (A i^i B)) vH (A i^i B))))) -> (y (_ B -> ((y vH A) i^i B) = (y vH (A i^i B)))))
40		sseq2 2079	. . . . . . . 8 |- (x = (y vH (A i^i B)) -> ((A i^i B) (_ x <-> (A i^i B) (_ (y vH (A i^i B))))
41		sseq1 2078	. . . . . . . 8 |- (x = (y vH (A i^i B)) -> (x (_ (A vH B) <-> (y vH (A i^i B)) (_ (A vH B))