# Metamath Proof Explorer

## Theorem dihmeet

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

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

### Proof

Step Hyp Ref Expression
1 dihmeet.b 𝐵 = ( Base ‘ 𝐾 )
2 dihmeet.m = ( meet ‘ 𝐾 )
3 dihmeet.h 𝐻 = ( LHyp ‘ 𝐾 )
4 dihmeet.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
6 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → 𝐾 ∈ HL )
7 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → 𝑋𝐵 )
8 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → 𝑌𝐵 )
9 5 2 6 7 8 meetval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
10 9 fveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝐼 ‘ ( 𝑋 𝑌 ) ) = ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) )
11 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 prssi ( ( 𝑋𝐵𝑌𝐵 ) → { 𝑋 , 𝑌 } ⊆ 𝐵 )
13 12 3adant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → { 𝑋 , 𝑌 } ⊆ 𝐵 )
14 prnzg ( 𝑋𝐵 → { 𝑋 , 𝑌 } ≠ ∅ )
15 14 3ad2ant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → { 𝑋 , 𝑌 } ≠ ∅ )
16 1 5 3 4 dihglb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( { 𝑋 , 𝑌 } ⊆ 𝐵 ∧ { 𝑋 , 𝑌 } ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼𝑥 ) )
17 11 13 15 16 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼𝑥 ) )
18 fveq2 ( 𝑥 = 𝑋 → ( 𝐼𝑥 ) = ( 𝐼𝑋 ) )
19 fveq2 ( 𝑥 = 𝑌 → ( 𝐼𝑥 ) = ( 𝐼𝑌 ) )
20 18 19 iinxprg ( ( 𝑋𝐵𝑌𝐵 ) → 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼𝑥 ) = ( ( 𝐼𝑋 ) ∩ ( 𝐼𝑌 ) ) )
21 20 3adant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼𝑥 ) = ( ( 𝐼𝑋 ) ∩ ( 𝐼𝑌 ) ) )
22 10 17 21 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝐼 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐼𝑋 ) ∩ ( 𝐼𝑌 ) ) )