Metamath Proof Explorer

Theorem dihmeet

Description: Isomorphism H of a lattice meet. (Contributed by NM, 13-Apr-2014)

Ref Expression
Hypotheses dihmeet.b ⊢ B = Base K
dihmeet.m ⊢ ∧ ˙ = meet ⁡ K
dihmeet.h ⊢ H = LHyp ⁡ K
dihmeet.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihmeet ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ∧ ˙ Y = I ⁡ X ∩ I ⁡ Y

Proof

Step Hyp Ref Expression
1 dihmeet.b ⊢ B = Base K
2 dihmeet.m ⊢ ∧ ˙ = meet ⁡ K
3 dihmeet.h ⊢ H = LHyp ⁡ K
4 dihmeet.i ⊢ I = DIsoH ⁡ K ⁡ W
5 eqid ⊢ glb ⁡ K = glb ⁡ K
6 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → K ∈ HL
7 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → X ∈ B
8 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
9 5 2 6 7 8 meetval ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y = glb ⁡ K ⁡ X Y
10 9 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ∧ ˙ Y = I ⁡ glb ⁡ K ⁡ X Y
11 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → K ∈ HL ∧ W ∈ H
12 prssi ⊢ X ∈ B ∧ Y ∈ B → X Y ⊆ B
13 12 3adant1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → X Y ⊆ B
14 prnzg ⊢ X ∈ B → X Y ≠ ∅
15 14 3ad2ant2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → X Y ≠ ∅
16 1 5 3 4 dihglb ⊢ K ∈ HL ∧ W ∈ H ∧ X Y ⊆ B ∧ X Y ≠ ∅ → I ⁡ glb ⁡ K ⁡ X Y = ⋂ x ∈ X Y I ⁡ x
17 11 13 15 16 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ glb ⁡ K ⁡ X Y = ⋂ x ∈ X Y I ⁡ x
18 fveq2 ⊢ x = X → I ⁡ x = I ⁡ X
19 fveq2 ⊢ x = Y → I ⁡ x = I ⁡ Y
20 18 19 iinxprg ⊢ X ∈ B ∧ Y ∈ B → ⋂ x ∈ X Y I ⁡ x = I ⁡ X ∩ I ⁡ Y
21 20 3adant1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → ⋂ x ∈ X Y I ⁡ x = I ⁡ X ∩ I ⁡ Y
22 10 17 21 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ∧ ˙ Y = I ⁡ X ∩ I ⁡ Y