Theorem dmdbr6ati

Description: Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sumdmdi.1	⊢ 𝐴 ∈ Cℋ
	sumdmdi.2	⊢ 𝐵 ∈ Cℋ
Assertion	dmdbr6ati	⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	⊢ 𝐴 ∈ Cℋ
2		sumdmdi.2	⊢ 𝐵 ∈ Cℋ
3		dmdbr3	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
4	1 2 3	mp2an	⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
5		chabs2	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ∩ ( 𝑥 ∨ℋ 𝐵 ) ) = 𝑥 )
6	2 5	mpan2	⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∩ ( 𝑥 ∨ℋ 𝐵 ) ) = 𝑥 )
7	6	ineq2d	⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝑥 ∩ ( 𝑥 ∨ℋ 𝐵 ) ) ) = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) )
8		incom	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝑥 ∩ ( 𝑥 ∨ℋ 𝐵 ) ) ) = ( ( 𝑥 ∩ ( 𝑥 ∨ℋ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) )
9		inass	⊢ ( ( 𝑥 ∩ ( 𝑥 ∨ℋ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝑥 ∩ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
10		incom	⊢ ( 𝑥 ∩ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝑥 )
11	8 9 10	3eqtri	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝑥 ∩ ( 𝑥 ∨ℋ 𝐵 ) ) ) = ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝑥 )
12	7 11	eqtr3di	⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝑥 ) )
13	12	adantr	⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝑥 ) )
14		ineq1	⊢ ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝑥 ) )
15	14	adantl	⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝑥 ) )
16	13 15	eqtr4d	⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) )
17	16	ralimiaa	⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) )
18	4 17	sylbi	⊢ ( 𝐴 𝑀ℋ* 𝐵 → ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) )
19		atelch	⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
20	19	imim1i	⊢ ( ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) ) → ( 𝑥 ∈ HAtoms → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) ) )
21	20	ralimi2	⊢ ( ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) → ∀ 𝑥 ∈ HAtoms ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) )
22	18 21	syl	⊢ ( 𝐴 𝑀ℋ* 𝐵 → ∀ 𝑥 ∈ HAtoms ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) )
23		inss1	⊢ ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 )
24		sseq1	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
25	23 24	mpbiri	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
26		incom	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) )
27		dfss2	⊢ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝑥 )
28	27	biimpi	⊢ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝑥 )
29	26 28	eqtrid	⊢ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = 𝑥 )
30	29	sseq1d	⊢ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
31	25 30	syl5ibcom	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
32	31	ralimi	⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) → ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
33	1 2	dmdbr5ati	⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
34	32 33	sylibr	⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) → 𝐴 𝑀ℋ* 𝐵 )
35	22 34	impbii	⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝑥 ) = ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∩ 𝑥 ) )