# Metamath Proof Explorer

## Theorem dihmeet

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

Ref Expression
Hypotheses dihmeet.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihmeet.m
dihmeet.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihmeet.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
Assertion dihmeet

### Proof

Step Hyp Ref Expression
1 dihmeet.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihmeet.m
3 dihmeet.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dihmeet.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
5 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
6 simp1l ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{HL}$
7 simp2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
8 simp3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
9 5 2 6 7 8 meetval
10 9 fveq2d
11 simp1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
12 prssi ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left\{{X},{Y}\right\}\subseteq {B}$
13 12 3adant1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left\{{X},{Y}\right\}\subseteq {B}$
14 prnzg ${⊢}{X}\in {B}\to \left\{{X},{Y}\right\}\ne \varnothing$
15 14 3ad2ant2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left\{{X},{Y}\right\}\ne \varnothing$
16 1 5 3 4 dihglb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left(\left\{{X},{Y}\right\}\subseteq {B}\wedge \left\{{X},{Y}\right\}\ne \varnothing \right)\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left(\left\{{X},{Y}\right\}\right)\right)=\bigcap _{{x}\in \left\{{X},{Y}\right\}}{I}\left({x}\right)$
17 11 13 15 16 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left(\left\{{X},{Y}\right\}\right)\right)=\bigcap _{{x}\in \left\{{X},{Y}\right\}}{I}\left({x}\right)$
18 fveq2 ${⊢}{x}={X}\to {I}\left({x}\right)={I}\left({X}\right)$
19 fveq2 ${⊢}{x}={Y}\to {I}\left({x}\right)={I}\left({Y}\right)$
20 18 19 iinxprg ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \bigcap _{{x}\in \left\{{X},{Y}\right\}}{I}\left({x}\right)={I}\left({X}\right)\cap {I}\left({Y}\right)$
21 20 3adant1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \bigcap _{{x}\in \left\{{X},{Y}\right\}}{I}\left({x}\right)={I}\left({X}\right)\cap {I}\left({Y}\right)$
22 10 17 21 3eqtrd