Theorem mdslj2i

Description: Meet preservation of the reverse mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslle1.1	⊢ 𝐴 ∈ Cℋ
	mdslle1.2	⊢ 𝐵 ∈ Cℋ
	mdslle1.3	⊢ 𝐶 ∈ Cℋ
	mdslle1.4	⊢ 𝐷 ∈ Cℋ
Assertion	mdslj2i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdslle1.1	⊢ 𝐴 ∈ Cℋ
2		mdslle1.2	⊢ 𝐵 ∈ Cℋ
3		mdslle1.3	⊢ 𝐶 ∈ Cℋ
4		mdslle1.4	⊢ 𝐷 ∈ Cℋ
5	3 4 1	lejdiri	⊢ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) )
6	5	a1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
7		ssin	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) )
8	7	bicomi	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) )
9	3 4 2	chlubi	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 )
10	9	bicomi	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ↔ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) )
11	8 10	anbi12i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) )
12		simpr	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐵 𝑀ℋ* 𝐴 )
13	1 3	chub2i	⊢ 𝐴 ⊆ ( 𝐶 ∨ℋ 𝐴 )
14	1 4	chub2i	⊢ 𝐴 ⊆ ( 𝐷 ∨ℋ 𝐴 )
15	13 14	ssini	⊢ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) )
16	15	a1i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) → 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
17	3 2 1	chlej1i	⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐵 ∨ℋ 𝐴 ) )
18	2 1	chjcomi	⊢ ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 )
19	17 18	sseqtrdi	⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
20		ssinss1	⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
21	19 20	syl	⊢ ( 𝐶 ⊆ 𝐵 → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
22	21	adantr	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
23	3 1	chjcli	⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
24	4 1	chjcli	⊢ ( 𝐷 ∨ℋ 𝐴 ) ∈ Cℋ
25	23 24	chincli	⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∈ Cℋ
26	1 2 25	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∈ Cℋ )
27		dmdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
28	26 27	mpan	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
29	12 16 22 28	syl3an	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )
30		inss1	⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐶 ∨ℋ 𝐴 )
31		ssrin	⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐶 ∨ℋ 𝐴 ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
32	30 31	ax-mp	⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 )
33		simpl	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
34		simpl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
35		simpl	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) → 𝐶 ⊆ 𝐵 )
36	1 2 3	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
37		mdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
38	36 37	mpan	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
39	33 34 35 38	syl3an	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
40	32 39	sseqtrid	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ 𝐶 )
41		inss2	⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐷 ∨ℋ 𝐴 )
42		ssrin	⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐷 ∨ℋ 𝐴 ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
43	41 42	ax-mp	⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 )
44		simpr	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 )
45		simpr	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) → 𝐷 ⊆ 𝐵 )
46	1 2 4	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
47		mdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
48	46 47	mpan	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
49	33 44 45 48	syl3an	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
50	43 49	sseqtrid	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ 𝐷 )
51	40 50	ssind	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) )
52	25 2	chincli	⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∈ Cℋ
53	3 4	chincli	⊢ ( 𝐶 ∩ 𝐷 ) ∈ Cℋ
54	52 53 1	chlej1i	⊢ ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
55	51 54	syl	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
56	29 55	eqsstrrd	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
57	56	3expb	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
58	11 57	sylan2b	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) )
59	6 58	eqssd	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) )