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

Theorem djh02 39808
Description: Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.)
Hypotheses
Ref Expression
djh01.h 𝐻 = (LHyp‘𝐾)
djh01.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
djh01.o 0 = (0g𝑈)
djh01.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
djh01.j = ((joinH‘𝐾)‘𝑊)
djh01.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
djh01.x (𝜑𝑋 ∈ ran 𝐼)
Assertion
Ref Expression
djh02 (𝜑 → ({ 0 } 𝑋) = 𝑋)

Proof of Theorem djh02
StepHypRef Expression
1 djh01.h . . 3 𝐻 = (LHyp‘𝐾)
2 djh01.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 eqid 2738 . . 3 (Base‘𝑈) = (Base‘𝑈)
4 djh01.j . . 3 = ((joinH‘𝐾)‘𝑊)
5 djh01.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
6 djh01.i . . . . 5 𝐼 = ((DIsoH‘𝐾)‘𝑊)
7 djh01.o . . . . 5 0 = (0g𝑈)
81, 6, 2, 7dih0rn 39679 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → { 0 } ∈ ran 𝐼)
91, 2, 6, 3dihrnss 39673 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ { 0 } ∈ ran 𝐼) → { 0 } ⊆ (Base‘𝑈))
105, 8, 9syl2anc2 586 . . 3 (𝜑 → { 0 } ⊆ (Base‘𝑈))
11 djh01.x . . . 4 (𝜑𝑋 ∈ ran 𝐼)
121, 2, 6, 3dihrnss 39673 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ ran 𝐼) → 𝑋 ⊆ (Base‘𝑈))
135, 11, 12syl2anc 585 . . 3 (𝜑𝑋 ⊆ (Base‘𝑈))
141, 2, 3, 4, 5, 10, 13djhcom 39800 . 2 (𝜑 → ({ 0 } 𝑋) = (𝑋 { 0 }))
151, 2, 7, 6, 4, 5, 11djh01 39807 . 2 (𝜑 → (𝑋 { 0 }) = 𝑋)
1614, 15eqtrd 2778 1 (𝜑 → ({ 0 } 𝑋) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wss 3909  {csn 4585  ran crn 5633  cfv 6494  (class class class)co 7352  Basecbs 17043  0gc0g 17281  HLchlt 37744  LHypclh 38379  DVecHcdvh 39473  DIsoHcdih 39623  joinHcdjh 39789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7665  ax-cnex 11066  ax-resscn 11067  ax-1cn 11068  ax-icn 11069  ax-addcl 11070  ax-addrcl 11071  ax-mulcl 11072  ax-mulrcl 11073  ax-mulcom 11074  ax-addass 11075  ax-mulass 11076  ax-distr 11077  ax-i2m1 11078  ax-1ne0 11079  ax-1rid 11080  ax-rnegex 11081  ax-rrecex 11082  ax-cnre 11083  ax-pre-lttri 11084  ax-pre-lttrn 11085  ax-pre-ltadd 11086  ax-pre-mulgt0 11087  ax-riotaBAD 37347
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-iin 4956  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7308  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7796  df-1st 7914  df-2nd 7915  df-tpos 8150  df-undef 8197  df-frecs 8205  df-wrecs 8236  df-recs 8310  df-rdg 8349  df-1o 8405  df-er 8607  df-map 8726  df-en 8843  df-dom 8844  df-sdom 8845  df-fin 8846  df-pnf 11150  df-mnf 11151  df-xr 11152  df-ltxr 11153  df-le 11154  df-sub 11346  df-neg 11347  df-nn 12113  df-2 12175  df-3 12176  df-4 12177  df-5 12178  df-6 12179  df-n0 12373  df-z 12459  df-uz 12723  df-fz 13380  df-struct 16979  df-sets 16996  df-slot 17014  df-ndx 17026  df-base 17044  df-ress 17073  df-plusg 17106  df-mulr 17107  df-sca 17109  df-vsca 17110  df-0g 17283  df-proset 18144  df-poset 18162  df-plt 18179  df-lub 18195  df-glb 18196  df-join 18197  df-meet 18198  df-p0 18274  df-p1 18275  df-lat 18281  df-clat 18348  df-mgm 18457  df-sgrp 18506  df-mnd 18517  df-submnd 18562  df-grp 18711  df-minusg 18712  df-sbg 18713  df-subg 18884  df-cntz 19056  df-lsm 19377  df-cmn 19523  df-abl 19524  df-mgp 19856  df-ur 19873  df-ring 19920  df-oppr 20002  df-dvdsr 20023  df-unit 20024  df-invr 20054  df-dvr 20065  df-drng 20140  df-lmod 20277  df-lss 20346  df-lsp 20386  df-lvec 20517  df-lsatoms 37370  df-oposet 37570  df-ol 37572  df-oml 37573  df-covers 37660  df-ats 37661  df-atl 37692  df-cvlat 37716  df-hlat 37745  df-llines 37893  df-lplanes 37894  df-lvols 37895  df-lines 37896  df-psubsp 37898  df-pmap 37899  df-padd 38191  df-lhyp 38383  df-laut 38384  df-ldil 38499  df-ltrn 38500  df-trl 38554  df-tendo 39150  df-edring 39152  df-disoa 39424  df-dvech 39474  df-dib 39534  df-dic 39568  df-dih 39624  df-doch 39743  df-djh 39790
This theorem is referenced by:  dihjat1lem  39823
  Copyright terms: Public domain W3C validator