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

Theorem dihglb2 39661
Description: Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014.)
Hypotheses
Ref Expression
dihglb.b 𝐵 = (Base‘𝐾)
dihglb.g 𝐺 = (glb‘𝐾)
dihglb.h 𝐻 = (LHyp‘𝐾)
dihglb.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihglb2.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihglb2.v 𝑉 = (Base‘𝑈)
Assertion
Ref Expression
dihglb2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (𝐼‘(𝐺‘{𝑥𝐵𝑆 ⊆ (𝐼𝑥)})) = {𝑦 ∈ ran 𝐼𝑆𝑦})
Distinct variable groups:   𝑥,𝐵   𝑥,𝐼   𝑥,𝐾   𝑥,𝑆,𝑦   𝑦,𝐵   𝑦,𝐻   𝑦,𝐼   𝑦,𝐾   𝑦,𝑆   𝑦,𝑉   𝑦,𝑊
Allowed substitution hints:   𝑈(𝑥,𝑦)   𝐺(𝑥,𝑦)   𝐻(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem dihglb2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 simpl 483 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 ssrab2 4025 . . . 4 {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ⊆ 𝐵
32a1i 11 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ⊆ 𝐵)
4 hlop 37680 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ OP)
54ad2antrr 723 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → 𝐾 ∈ OP)
6 dihglb.b . . . . . . 7 𝐵 = (Base‘𝐾)
7 eqid 2736 . . . . . . 7 (1.‘𝐾) = (1.‘𝐾)
86, 7op1cl 37503 . . . . . 6 (𝐾 ∈ OP → (1.‘𝐾) ∈ 𝐵)
95, 8syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (1.‘𝐾) ∈ 𝐵)
10 simpr 485 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → 𝑆𝑉)
11 dihglb.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
12 dihglb.i . . . . . . . 8 𝐼 = ((DIsoH‘𝐾)‘𝑊)
13 dihglb2.u . . . . . . . 8 𝑈 = ((DVecH‘𝐾)‘𝑊)
14 dihglb2.v . . . . . . . 8 𝑉 = (Base‘𝑈)
157, 11, 12, 13, 14dih1 39605 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐼‘(1.‘𝐾)) = 𝑉)
1615adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (𝐼‘(1.‘𝐾)) = 𝑉)
1710, 16sseqtrrd 3973 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → 𝑆 ⊆ (𝐼‘(1.‘𝐾)))
18 fveq2 6826 . . . . . . 7 (𝑥 = (1.‘𝐾) → (𝐼𝑥) = (𝐼‘(1.‘𝐾)))
1918sseq2d 3964 . . . . . 6 (𝑥 = (1.‘𝐾) → (𝑆 ⊆ (𝐼𝑥) ↔ 𝑆 ⊆ (𝐼‘(1.‘𝐾))))
2019elrab 3634 . . . . 5 ((1.‘𝐾) ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ↔ ((1.‘𝐾) ∈ 𝐵𝑆 ⊆ (𝐼‘(1.‘𝐾))))
219, 17, 20sylanbrc 583 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (1.‘𝐾) ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)})
2221ne0d 4283 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ≠ ∅)
23 dihglb.g . . . 4 𝐺 = (glb‘𝐾)
246, 23, 11, 12dihglb 39660 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ({𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ⊆ 𝐵 ∧ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ≠ ∅)) → (𝐼‘(𝐺‘{𝑥𝐵𝑆 ⊆ (𝐼𝑥)})) = 𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} (𝐼𝑧))
251, 3, 22, 24syl12anc 834 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (𝐼‘(𝐺‘{𝑥𝐵𝑆 ⊆ (𝐼𝑥)})) = 𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} (𝐼𝑧))
26 fvex 6839 . . . 4 (𝐼𝑧) ∈ V
2726dfiin2 4982 . . 3 𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} (𝐼𝑧) = {𝑦 ∣ ∃𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)}𝑦 = (𝐼𝑧)}
286, 11, 12dihfn 39587 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐼 Fn 𝐵)
2928ad2antrr 723 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) ∧ 𝑆𝑦) → 𝐼 Fn 𝐵)
30 fvelrnb 6887 . . . . . . . . . . 11 (𝐼 Fn 𝐵 → (𝑦 ∈ ran 𝐼 ↔ ∃𝑧𝐵 (𝐼𝑧) = 𝑦))
3129, 30syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) ∧ 𝑆𝑦) → (𝑦 ∈ ran 𝐼 ↔ ∃𝑧𝐵 (𝐼𝑧) = 𝑦))
32 eqcom 2743 . . . . . . . . . . . 12 ((𝐼𝑧) = 𝑦𝑦 = (𝐼𝑧))
3332rexbii 3093 . . . . . . . . . . 11 (∃𝑧𝐵 (𝐼𝑧) = 𝑦 ↔ ∃𝑧𝐵 𝑦 = (𝐼𝑧))
34 df-rex 3071 . . . . . . . . . . 11 (∃𝑧𝐵 𝑦 = (𝐼𝑧) ↔ ∃𝑧(𝑧𝐵𝑦 = (𝐼𝑧)))
3533, 34bitri 274 . . . . . . . . . 10 (∃𝑧𝐵 (𝐼𝑧) = 𝑦 ↔ ∃𝑧(𝑧𝐵𝑦 = (𝐼𝑧)))
3631, 35bitrdi 286 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) ∧ 𝑆𝑦) → (𝑦 ∈ ran 𝐼 ↔ ∃𝑧(𝑧𝐵𝑦 = (𝐼𝑧))))
3736ex 413 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (𝑆𝑦 → (𝑦 ∈ ran 𝐼 ↔ ∃𝑧(𝑧𝐵𝑦 = (𝐼𝑧)))))
3837pm5.32rd 578 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → ((𝑦 ∈ ran 𝐼𝑆𝑦) ↔ (∃𝑧(𝑧𝐵𝑦 = (𝐼𝑧)) ∧ 𝑆𝑦)))
39 df-rex 3071 . . . . . . . 8 (∃𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)}𝑦 = (𝐼𝑧) ↔ ∃𝑧(𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ∧ 𝑦 = (𝐼𝑧)))
40 fveq2 6826 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐼𝑥) = (𝐼𝑧))
4140sseq2d 3964 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑆 ⊆ (𝐼𝑥) ↔ 𝑆 ⊆ (𝐼𝑧)))
4241elrab 3634 . . . . . . . . . . 11 (𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ↔ (𝑧𝐵𝑆 ⊆ (𝐼𝑧)))
4342anbi1i 624 . . . . . . . . . 10 ((𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ∧ 𝑦 = (𝐼𝑧)) ↔ ((𝑧𝐵𝑆 ⊆ (𝐼𝑧)) ∧ 𝑦 = (𝐼𝑧)))
44 sseq2 3958 . . . . . . . . . . . 12 (𝑦 = (𝐼𝑧) → (𝑆𝑦𝑆 ⊆ (𝐼𝑧)))
4544anbi2d 629 . . . . . . . . . . 11 (𝑦 = (𝐼𝑧) → ((𝑧𝐵𝑆𝑦) ↔ (𝑧𝐵𝑆 ⊆ (𝐼𝑧))))
4645pm5.32ri 576 . . . . . . . . . 10 (((𝑧𝐵𝑆𝑦) ∧ 𝑦 = (𝐼𝑧)) ↔ ((𝑧𝐵𝑆 ⊆ (𝐼𝑧)) ∧ 𝑦 = (𝐼𝑧)))
47 an32 643 . . . . . . . . . 10 (((𝑧𝐵𝑆𝑦) ∧ 𝑦 = (𝐼𝑧)) ↔ ((𝑧𝐵𝑦 = (𝐼𝑧)) ∧ 𝑆𝑦))
4843, 46, 473bitr2i 298 . . . . . . . . 9 ((𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ∧ 𝑦 = (𝐼𝑧)) ↔ ((𝑧𝐵𝑦 = (𝐼𝑧)) ∧ 𝑆𝑦))
4948exbii 1849 . . . . . . . 8 (∃𝑧(𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} ∧ 𝑦 = (𝐼𝑧)) ↔ ∃𝑧((𝑧𝐵𝑦 = (𝐼𝑧)) ∧ 𝑆𝑦))
50 19.41v 1952 . . . . . . . 8 (∃𝑧((𝑧𝐵𝑦 = (𝐼𝑧)) ∧ 𝑆𝑦) ↔ (∃𝑧(𝑧𝐵𝑦 = (𝐼𝑧)) ∧ 𝑆𝑦))
5139, 49, 503bitrri 297 . . . . . . 7 ((∃𝑧(𝑧𝐵𝑦 = (𝐼𝑧)) ∧ 𝑆𝑦) ↔ ∃𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)}𝑦 = (𝐼𝑧))
5238, 51bitr2di 287 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (∃𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)}𝑦 = (𝐼𝑧) ↔ (𝑦 ∈ ran 𝐼𝑆𝑦)))
5352abbidv 2805 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → {𝑦 ∣ ∃𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)}𝑦 = (𝐼𝑧)} = {𝑦 ∣ (𝑦 ∈ ran 𝐼𝑆𝑦)})
54 df-rab 3404 . . . . 5 {𝑦 ∈ ran 𝐼𝑆𝑦} = {𝑦 ∣ (𝑦 ∈ ran 𝐼𝑆𝑦)}
5553, 54eqtr4di 2794 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → {𝑦 ∣ ∃𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)}𝑦 = (𝐼𝑧)} = {𝑦 ∈ ran 𝐼𝑆𝑦})
5655inteqd 4900 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → {𝑦 ∣ ∃𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)}𝑦 = (𝐼𝑧)} = {𝑦 ∈ ran 𝐼𝑆𝑦})
5727, 56eqtrid 2788 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → 𝑧 ∈ {𝑥𝐵𝑆 ⊆ (𝐼𝑥)} (𝐼𝑧) = {𝑦 ∈ ran 𝐼𝑆𝑦})
5825, 57eqtrd 2776 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝑉) → (𝐼‘(𝐺‘{𝑥𝐵𝑆 ⊆ (𝐼𝑥)})) = {𝑦 ∈ ran 𝐼𝑆𝑦})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wex 1780  wcel 2105  {cab 2713  wne 2940  wrex 3070  {crab 3403  wss 3898  c0 4270   cint 4895   ciin 4943  ran crn 5622   Fn wfn 6475  cfv 6480  Basecbs 17010  glbcglb 18126  1.cp1 18240  OPcops 37490  HLchlt 37668  LHypclh 38303  DVecHcdvh 39397  DIsoHcdih 39547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-riotaBAD 37271
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-1st 7900  df-2nd 7901  df-tpos 8113  df-undef 8160  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-er 8570  df-map 8689  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-n0 12336  df-z 12422  df-uz 12685  df-fz 13342  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-sca 17076  df-vsca 17077  df-0g 17250  df-proset 18111  df-poset 18129  df-plt 18146  df-lub 18162  df-glb 18163  df-join 18164  df-meet 18165  df-p0 18241  df-p1 18242  df-lat 18248  df-clat 18315  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-grp 18677  df-minusg 18678  df-sbg 18679  df-subg 18849  df-cntz 19020  df-lsm 19338  df-cmn 19484  df-abl 19485  df-mgp 19817  df-ur 19834  df-ring 19881  df-oppr 19958  df-dvdsr 19979  df-unit 19980  df-invr 20010  df-dvr 20021  df-drng 20096  df-lmod 20232  df-lss 20301  df-lsp 20341  df-lvec 20472  df-lsatoms 37294  df-oposet 37494  df-ol 37496  df-oml 37497  df-covers 37584  df-ats 37585  df-atl 37616  df-cvlat 37640  df-hlat 37669  df-llines 37817  df-lplanes 37818  df-lvols 37819  df-lines 37820  df-psubsp 37822  df-pmap 37823  df-padd 38115  df-lhyp 38307  df-laut 38308  df-ldil 38423  df-ltrn 38424  df-trl 38478  df-tendo 39074  df-edring 39076  df-disoa 39348  df-dvech 39398  df-dib 39458  df-dic 39492  df-dih 39548
This theorem is referenced by:  dochval2  39671
  Copyright terms: Public domain W3C validator