Theorem mdslle1i

Description: Order preservation of the one-to-one onto 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	mdslle1i	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐶 ⊆ 𝐷 ↔ ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdslle1.1	⊢ 𝐴 ∈ Cℋ
2		mdslle1.2	⊢ 𝐵 ∈ Cℋ
3		mdslle1.3	⊢ 𝐶 ∈ Cℋ
4		mdslle1.4	⊢ 𝐷 ∈ Cℋ
5		ssrin	⊢ ( 𝐶 ⊆ 𝐷 → ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) )
6	3 2	chincli	⊢ ( 𝐶 ∩ 𝐵 ) ∈ Cℋ
7	4 2	chincli	⊢ ( 𝐷 ∩ 𝐵 ) ∈ Cℋ
8	6 7 1	chlej1i	⊢ ( ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
9		id	⊢ ( 𝐵 𝑀ℋ* 𝐴 → 𝐵 𝑀ℋ* 𝐴 )
10		ssin	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
11	10	bicomi	⊢ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ↔ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) )
12	11	simplbi	⊢ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) → 𝐴 ⊆ 𝐶 )
13	1 2	chjcli	⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
14	3 4 13	chlubi	⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
15	14	bicomi	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
16	15	simplbi	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
17	1 2 3	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
18		dmdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
19	17 18	mpan	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
20	9 12 16 19	syl3an	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
21	11	simprbi	⊢ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) → 𝐴 ⊆ 𝐷 )
22	15	simprbi	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
23	1 2 4	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
24		dmdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
25	23 24	mpan	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
26	9 21 22 25	syl3an	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
27	20 26	sseq12d	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) ↔ 𝐶 ⊆ 𝐷 ) )
28	8 27	imbitrid	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → 𝐶 ⊆ 𝐷 ) )
29	5 28	impbid2	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐶 ⊆ 𝐷 ↔ ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) ) )