This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ∩ ( 𝐼 ‘ 𝑊 ) ) )