dihglblem4 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihglblem4		Structured version Visualization version GIF version

Theorem dihglblem4 41874

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

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

**Assertion**
Ref	Expression
dihglblem4	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Distinct variable groups: 𝑥,𝑢,𝑣, ∧ 𝑥, ≤ 𝑥,𝐵,𝑢 𝑥,𝐺 𝑥,𝐻 𝑥,𝐾 𝑥,𝑆,𝑢,𝑣 𝑥,𝑇 𝑥,𝑊,𝑢,𝑣 𝑢, ≤ ,𝑣 𝑣,𝐵 𝑢,𝐺,𝑣 𝑢,𝐻,𝑣 𝑢,𝐾,𝑣 𝑥,𝐼 Allowed substitution hints: 𝑇(𝑣,𝑢) 𝐼(𝑣,𝑢) 𝐽(𝑥,𝑣,𝑢)

**Proof of Theorem dihglblem4**
Step	Hyp	Ref	Expression
1		hlclat 39935	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
2	1	ad3antrrr 740	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ CLat)
3		simplrl 786	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝐵)
4		simpr 488	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
5		dihglblem.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
6		dihglblem.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
7		dihglblem.g	. . . . . 6 ⊢ 𝐺 = (glb‘𝐾)
8	5, 6, 7	clatglble 18530	. . . . 5 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
9	2, 3, 4, 8	syl3anc 1389	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
10		simpll 776	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
11	5, 7	clatglbcl 18518	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
12	2, 3, 11	syl2anc 593	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵)
13	3, 4	sseldd 3937	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
14		dihglblem.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
15		dihglblem.ih	. . . . . 6 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
16	5, 6, 14, 15	dihord 41841	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺‘𝑆) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → ((𝐼‘(𝐺‘𝑆)) ⊆ (𝐼‘𝑥) ↔ (𝐺‘𝑆) ≤ 𝑥))
17	10, 12, 13, 16	syl3anc 1389	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → ((𝐼‘(𝐺‘𝑆)) ⊆ (𝐼‘𝑥) ↔ (𝐺‘𝑆) ≤ 𝑥))
18	9, 17	mpbird 259	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) ∧ 𝑥 ∈ 𝑆) → (𝐼‘(𝐺‘𝑆)) ⊆ (𝐼‘𝑥))
19	18	ralrimiva 3153	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → ∀𝑥 ∈ 𝑆 (𝐼‘(𝐺‘𝑆)) ⊆ (𝐼‘𝑥))
20		ssiin 5012	. 2 ⊢ ((𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 (𝐼‘(𝐺‘𝑆)) ⊆ (𝐼‘𝑥))
21	19, 20	sylibr 236	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 ∃wrex 3085 {crab 3413 ⊆ wss 3904 ∅c0 4285 ∩ ciin 4949 class class class wbr 5099 ‘cfv 6515 (class class class)co 7390 Basecbs 17226 lecple 17274 glbcglb 18323 meetcmee 18325 CLatccla 18511 HLchlt 39927 LHypclh 40561 DIsoBcdib 41715 DIsoHcdih 41805

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7712 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-riotaBAD 39530

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-iin 4951 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-tpos 8199 df-undef 8246 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-er 8671 df-map 8803 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-pnf 11213 df-mnf 11214 df-xr 11215 df-ltxr 11216 df-le 11217 df-sub 11411 df-neg 11412 df-nn 12206 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-n0 12477 df-z 12564 df-uz 12835 df-fz 13508 df-struct 17164 df-sets 17181 df-slot 17199 df-ndx 17211 df-base 17227 df-ress 17248 df-plusg 17280 df-mulr 17281 df-sca 17283 df-vsca 17284 df-0g 17451 df-proset 18307 df-poset 18326 df-plt 18341 df-lub 18357 df-glb 18358 df-join 18359 df-meet 18360 df-p0 18436 df-p1 18437 df-lat 18445 df-clat 18512 df-mgm 18655 df-sgrp 18734 df-mnd 18750 df-submnd 18799 df-grp 18959 df-minusg 18960 df-sbg 18961 df-subg 19146 df-cntz 19338 df-lsm 19657 df-cmn 19803 df-abl 19804 df-mgp 20168 df-rng 20180 df-ur 20209 df-ring 20262 df-oppr 20363 df-dvdsr 20383 df-unit 20384 df-invr 20414 df-dvr 20427 df-drng 20758 df-lmod 20907 df-lss 20977 df-lsp 21017 df-lvec 21148 df-oposet 39753 df-ol 39755 df-oml 39756 df-covers 39843 df-ats 39844 df-atl 39875 df-cvlat 39899 df-hlat 39928 df-llines 40075 df-lplanes 40076 df-lvols 40077 df-lines 40078 df-psubsp 40080 df-pmap 40081 df-padd 40373 df-lhyp 40565 df-laut 40566 df-ldil 40681 df-ltrn 40682 df-trl 40736 df-tendo 41332 df-edring 41334 df-disoa 41606 df-dvech 41656 df-dib 41716 df-dic 41750 df-dih 41806

This theorem is referenced by: dihglblem6 41917

W3C validator