This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihglblem3aN

Description: Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihglblem.l ⊢ ≤ = ( le ‘ 𝐾 )
dihglblem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihglblem.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
dihglblem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem.t ⊢ 𝑇 = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) }
dihglblem.i ⊢ 𝐽 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dihglblem.ih ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihglblem3aN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 dihglblem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihglblem.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihglblem.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dihglblem.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
5 dihglblem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dihglblem.t ⊢ 𝑇 = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) }
7 dihglblem.i ⊢ 𝐽 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8 dihglblem.ih ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9 1 2 3 4 5 6 dihglblem2N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ 𝑇 ) )
10 9 3adant2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ 𝑇 ) )
11 10 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑇 ) ) )
12 1 2 3 4 5 6 7 8 dihglblem3N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑇 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) )
13 11 12 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) )