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

Metamath Proof Explorer

Theorem dihglblem5

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

Ref Expression
Hypotheses dihglblem5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihglblem5.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
dihglblem5.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem5.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihglblem5.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihglblem5.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion dihglblem5 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 dihglblem5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihglblem5.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
3 dihglblem5.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihglblem5.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dihglblem5.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6 dihglblem5.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
7 fvex ⊢ ( 𝐼 ‘ 𝑥 ) ∈ V
8 7 dfiin2 ⊢ ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) }
9 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 3 4 9 dvhlmod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → 𝑈 ∈ LMod )
11 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑇 ⊆ 𝐵 )
13 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ 𝑇 )
14 12 13 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ 𝐵 )
15 1 3 5 4 6 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
16 11 14 15 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
17 16 ralrimiva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ∀ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
18 uniiunlem ⊢ ( ∀ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ⊆ 𝑆 ) )
19 17 18 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ( ∀ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ⊆ 𝑆 ) )
20 17 19 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ⊆ 𝑆 )
21 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → 𝑇 ≠ ∅ )
22 n0 ⊢ ( 𝑇 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑇 )
23 21 22 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ∃ 𝑥 𝑥 ∈ 𝑇 )
24 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 )
25 24 nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) }
26 nfcv ⊢ Ⅎ 𝑥 ∅
27 25 26 nfne ⊢ Ⅎ 𝑥 { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ≠ ∅
28 7 elabrex ⊢ ( 𝑥 ∈ 𝑇 → ( 𝐼 ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } )
29 28 ne0d ⊢ ( 𝑥 ∈ 𝑇 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ≠ ∅ )
30 27 29 exlimi ⊢ ( ∃ 𝑥 𝑥 ∈ 𝑇 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ≠ ∅ )
31 23 30 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ≠ ∅ )
32 6 lssintcl ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ⊆ 𝑆 ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ≠ ∅ ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ∈ 𝑆 )
33 10 20 31 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑇 𝑦 = ( 𝐼 ‘ 𝑥 ) } ∈ 𝑆 )
34 8 33 eqeltrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )