Metamath Proof Explorer

Theorem diameetN

Description: Partial isomorphism A of a lattice meet. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diam.m ⊢ ∧ = ( meet ‘ 𝐾 )
diam.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diam.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diameetN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 diam.m ⊢ ∧ = ( meet ‘ 𝐾 )
2 diam.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 diam.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
5 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → 𝐾 ∈ HL )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 3 diadmclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
8 7 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
9 6 2 3 diadmclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ dom 𝐼 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
10 9 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
11 4 1 5 8 10 meetval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → ( 𝑋 ∧ 𝑌 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
12 11 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) )
13 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 prssi ⊢ ( ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) → { 𝑋 , 𝑌 } ⊆ dom 𝐼 )
15 14 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → { 𝑋 , 𝑌 } ⊆ dom 𝐼 )
16 prnzg ⊢ ( 𝑋 ∈ dom 𝐼 → { 𝑋 , 𝑌 } ≠ ∅ )
17 16 ad2antrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → { 𝑋 , 𝑌 } ≠ ∅ )
18 4 2 3 diaglbN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( { 𝑋 , 𝑌 } ⊆ dom 𝐼 ∧ { 𝑋 , 𝑌 } ≠ ∅ ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) )
19 13 15 17 18 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) )
20 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑋 ) )
21 fveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑌 ) )
22 20 21 iinxprg ⊢ ( ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
23 22 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
24 12 19 23 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )