Metamath Proof Explorer

Theorem dihmeetcN

Description: Isomorphism H of a lattice meet when the meet is not under the fiducial hyperplane W . (Contributed by NM, 26-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 dihmeetcN ( ( ( 𝐾 ∈ 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 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝐾 ∈ HL )
8 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑋 ∈ 𝐵 )
9 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑌 ∈ 𝐵 )
10 6 3 7 8 9 meetval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝑋 ∧ 𝑌 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
11 10 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) )
12 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 prssi ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → { 𝑋 , 𝑌 } ⊆ 𝐵 )
14 13 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → { 𝑋 , 𝑌 } ⊆ 𝐵 )
15 prnzg ⊢ ( 𝑋 ∈ 𝐵 → { 𝑋 , 𝑌 } ≠ ∅ )
16 8 15 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → { 𝑋 , 𝑌 } ≠ ∅ )
17 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 )
18 10 breq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ↔ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ≤ 𝑊 ) )
19 17 18 mtbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ¬ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ≤ 𝑊 )
20 1 6 4 5 2 dihglbcN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( { 𝑋 , 𝑌 } ⊆ 𝐵 ∧ { 𝑋 , 𝑌 } ≠ ∅ ) ∧ ¬ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ≤ 𝑊 ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) )
21 12 14 16 19 20 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) )
22 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑋 ) )
23 fveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑌 ) )
24 22 23 iinxprg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
25 24 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
26 11 21 25 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )