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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )