Theorem mdslmd2i

Description: Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2 (join version). (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	⊢ 𝐴 ∈ Cℋ
2		mdslmd.2	⊢ 𝐵 ∈ Cℋ
3		mdslmd.3	⊢ 𝐶 ∈ Cℋ
4		mdslmd.4	⊢ 𝐷 ∈ Cℋ
5	3 4	chjcli	⊢ ( 𝐶 ∨ℋ 𝐷 ) ∈ Cℋ
6	5 2 1	chlej1i	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → ( ( 𝐶 ∨ℋ 𝐷 ) ∨ℋ 𝐴 ) ⊆ ( 𝐵 ∨ℋ 𝐴 ) )
7	3 4 1	chjjdiri	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ∨ℋ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) )
8	2 1	chjcomi	⊢ ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 )
9	6 7 8	3sstr3g	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
10	9	adantl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
11	1 3	chub2i	⊢ 𝐴 ⊆ ( 𝐶 ∨ℋ 𝐴 )
12	1 4	chub2i	⊢ 𝐴 ⊆ ( 𝐷 ∨ℋ 𝐴 )
13	11 12	ssini	⊢ 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) )
14	10 13	jctil	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
15	3 1	chjcli	⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
16	4 1	chjcli	⊢ ( 𝐷 ∨ℋ 𝐴 ) ∈ Cℋ
17	1 2 15 16	mdslmd1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐷 ∨ℋ 𝐴 ) ) ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ ( 𝐷 ∨ℋ 𝐴 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ ( 𝐷 ∨ℋ 𝐴 ) ↔ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
18	14 17	sylan2	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ ( 𝐷 ∨ℋ 𝐴 ) ↔ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
19		id	⊢ ( 𝐴 𝑀ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵 )
20		inss1	⊢ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐶
21		sstr	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
22	20 21	mpan2	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
23	3 4	chub1i	⊢ 𝐶 ⊆ ( 𝐶 ∨ℋ 𝐷 )
24		sstr	⊢ ( ( 𝐶 ⊆ ( 𝐶 ∨ℋ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → 𝐶 ⊆ 𝐵 )
25	23 24	mpan	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → 𝐶 ⊆ 𝐵 )
26	1 2 3	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
27		mdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
28	26 27	mpan	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
29	19 22 25 28	syl3an	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )
30		inss2	⊢ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐷
31		sstr	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 )
32	30 31	mpan2	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 )
33	4 3	chub2i	⊢ 𝐷 ⊆ ( 𝐶 ∨ℋ 𝐷 )
34		sstr	⊢ ( ( 𝐷 ⊆ ( 𝐶 ∨ℋ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → 𝐷 ⊆ 𝐵 )
35	33 34	mpan	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 → 𝐷 ⊆ 𝐵 )
36	1 2 4	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
37		mdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
38	36 37	mpan	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
39	19 32 35 38	syl3an	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐷 )
40	29 39	breq12d	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ↔ 𝐶 𝑀ℋ 𝐷 ) )
41	40	3expb	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ↔ 𝐶 𝑀ℋ 𝐷 ) )
42	41	adantlr	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) 𝑀ℋ ( ( 𝐷 ∨ℋ 𝐴 ) ∩ 𝐵 ) ↔ 𝐶 𝑀ℋ 𝐷 ) )
43	18 42	bitr2d	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ ( 𝐷 ∨ℋ 𝐴 ) ) )