dihglblem4

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

	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	dihglblem4	⊢ ( ( ( 𝐾 ∈ 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		hlclat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
10	9	ad3antrrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ CLat )
11		simplrl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
12		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
13	1 2 4	clatglble	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 )
14	10 11 12 13	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 )
15		simpll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16	1 4	clatglbcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
17	10 11 16	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
18	11 12	sseldd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
19	1 2 5 8	dihord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 ) )
20	15 17 18 19	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 ) )
21	14 20	mpbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) )
22	21	ralrimiva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) )
23		ssiin	⊢ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) )
24	22 23	sylibr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )

Metamath Proof Explorer

Theorem dihglblem4

Proof