Theorem mddmdin0i

Description: If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of Holland p. 1524 to hold. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mddmdin0.1	⊢ 𝐴 ∈ Cℋ
	mddmdin0.2	⊢ 𝐵 ∈ Cℋ
	mddmdin0.3	⊢ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( 𝑥 𝑀ℋ* 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = 0ℋ ) → 𝑥 𝑀ℋ 𝑦 )
Assertion	mddmdin0i	⊢ ( 𝐴 𝑀ℋ* 𝐵 → 𝐴 𝑀ℋ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mddmdin0.1	⊢ 𝐴 ∈ Cℋ
2		mddmdin0.2	⊢ 𝐵 ∈ Cℋ
3		mddmdin0.3	⊢ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( 𝑥 𝑀ℋ* 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = 0ℋ ) → 𝑥 𝑀ℋ 𝑦 )
4		inindir	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
5	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
6	5	chocini	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = 0ℋ
7	4 6	eqtr3i	⊢ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = 0ℋ
8	5	choccli	⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ
9	1 8	chincli	⊢ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∈ Cℋ
10	2 8	chincli	⊢ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∈ Cℋ
11		breq1	⊢ ( 𝑥 = ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑥 𝑀ℋ* 𝑦 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* 𝑦 ) )
12		ineq1	⊢ ( 𝑥 = ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) )
13	12	eqeq1d	⊢ ( 𝑥 = ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) = 0ℋ ↔ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) = 0ℋ ) )
14	11 13	anbi12d	⊢ ( 𝑥 = ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑥 𝑀ℋ* 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = 0ℋ ) ↔ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* 𝑦 ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) = 0ℋ ) ) )
15		breq1	⊢ ( 𝑥 = ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑥 𝑀ℋ 𝑦 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ 𝑦 ) )
16	14 15	imbi12d	⊢ ( 𝑥 = ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝑥 𝑀ℋ* 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = 0ℋ ) → 𝑥 𝑀ℋ 𝑦 ) ↔ ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* 𝑦 ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) = 0ℋ ) → ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ 𝑦 ) ) )
17		breq2	⊢ ( 𝑦 = ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* 𝑦 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
18		ineq2	⊢ ( 𝑦 = ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) = ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
19	18	eqeq1d	⊢ ( 𝑦 = ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) = 0ℋ ↔ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = 0ℋ ) )
20	17 19	anbi12d	⊢ ( 𝑦 = ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* 𝑦 ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) = 0ℋ ) ↔ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = 0ℋ ) ) )
21		breq2	⊢ ( 𝑦 = ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ 𝑦 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
22	20 21	imbi12d	⊢ ( 𝑦 = ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* 𝑦 ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ 𝑦 ) = 0ℋ ) → ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ 𝑦 ) ↔ ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = 0ℋ ) → ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
23	16 22	rspc2v	⊢ ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∈ Cℋ ∧ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( 𝑥 𝑀ℋ* 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = 0ℋ ) → 𝑥 𝑀ℋ 𝑦 ) → ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = 0ℋ ) → ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
24	9 10 23	mp2an	⊢ ( ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( 𝑥 𝑀ℋ* 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = 0ℋ ) → 𝑥 𝑀ℋ 𝑦 ) → ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = 0ℋ ) → ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
25	3 24	ax-mp	⊢ ( ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∩ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = 0ℋ ) → ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
26	7 25	mpan2	⊢ ( ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
27	1 2	dmdcompli	⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ* ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
28	1 2	mdcompli	⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
29	26 27 28	3imtr4i	⊢ ( 𝐴 𝑀ℋ* 𝐵 → 𝐴 𝑀ℋ 𝐵 )