Theorem dihmeetbclemN

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetc.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihmeetc.l	⊢ ≤ = ( le ‘ 𝐾 )
	dihmeetc.m	⊢ ∧ = ( meet ‘ 𝐾 )
	dihmeetc.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihmeetc.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dihmeetbclemN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ∩ ( 𝐼 ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihmeetc.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihmeetc.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dihmeetc.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		dihmeetc.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		dihmeetc.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 )
7		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝐾 ∈ HL )
8	7	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝐾 ∈ Lat )
9		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑋 ∈ 𝐵 )
10		simp2r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑌 ∈ 𝐵 )
11	1 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
12	8 9 10 11	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
13		simp1r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑊 ∈ 𝐻 )
14	1 4	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
15	13 14	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑊 ∈ 𝐵 )
16	1 2 3	latleeqm1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ↔ ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑊 ) = ( 𝑋 ∧ 𝑌 ) ) )
17	8 12 15 16	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ↔ ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑊 ) = ( 𝑋 ∧ 𝑌 ) ) )
18	6 17	mpbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑊 ) = ( 𝑋 ∧ 𝑌 ) )
19		hlol	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
20	7 19	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝐾 ∈ OL )
21	1 3	latmassOLD	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑊 ) = ( 𝑋 ∧ ( 𝑌 ∧ 𝑊 ) ) )
22	20 9 10 15 21	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑊 ) = ( 𝑋 ∧ ( 𝑌 ∧ 𝑊 ) ) )
23	18 22	eqtr3d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑌 ∧ 𝑊 ) ) )
24	23	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( 𝐼 ‘ ( 𝑋 ∧ ( 𝑌 ∧ 𝑊 ) ) ) )
25		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26	1 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
27	8 10 15 26	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
28	1 2 3	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑊 ) ≤ 𝑊 )
29	8 10 15 28	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝑌 ∧ 𝑊 ) ≤ 𝑊 )
30	1 2 3 4 5	dihmeetbN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ ( 𝑌 ∧ 𝑊 ) ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) )
31	25 9 27 29 30	syl112anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ ( 𝑌 ∧ 𝑊 ) ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) )
32	1 2	latref	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐵 ) → 𝑊 ≤ 𝑊 )
33	8 15 32	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑊 ≤ 𝑊 )
34	1 2 3 4 5	dihmeetbN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑊 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )
35	25 10 15 33 34	syl112anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )
36	35	ineq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑊 ) ) ) )
37	24 31 36	3eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑊 ) ) ) )
38		inass	⊢ ( ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ∩ ( 𝐼 ‘ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )
39	37 38	eqtr4di	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ∩ ( 𝐼 ‘ 𝑊 ) ) )