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

Theorem docavalN 35889
Description: Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
docaval.j = (join‘𝐾)
docaval.m = (meet‘𝐾)
docaval.o = (oc‘𝐾)
docaval.h 𝐻 = (LHyp‘𝐾)
docaval.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
docaval.i 𝐼 = ((DIsoA‘𝐾)‘𝑊)
docaval.n 𝑁 = ((ocA‘𝐾)‘𝑊)
Assertion
Ref Expression
docavalN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇) → (𝑁𝑋) = (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊)))
Distinct variable groups:   𝑧,𝐾   𝑧,𝐼   𝑧,𝑊   𝑧,𝑇   𝑧,𝑋
Allowed substitution hints:   𝐻(𝑧)   (𝑧)   (𝑧)   𝑁(𝑧)   (𝑧)

Proof of Theorem docavalN
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 docaval.j . . . . 5 = (join‘𝐾)
2 docaval.m . . . . 5 = (meet‘𝐾)
3 docaval.o . . . . 5 = (oc‘𝐾)
4 docaval.h . . . . 5 𝐻 = (LHyp‘𝐾)
5 docaval.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
6 docaval.i . . . . 5 𝐼 = ((DIsoA‘𝐾)‘𝑊)
7 docaval.n . . . . 5 𝑁 = ((ocA‘𝐾)‘𝑊)
81, 2, 3, 4, 5, 6, 7docafvalN 35888 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑁 = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊))))
98adantr 481 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇) → 𝑁 = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊))))
109fveq1d 6150 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇) → (𝑁𝑋) = ((𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊)))‘𝑋))
11 fvex 6158 . . . . . . 7 ((LTrn‘𝐾)‘𝑊) ∈ V
125, 11eqeltri 2694 . . . . . 6 𝑇 ∈ V
1312elpw2 4788 . . . . 5 (𝑋 ∈ 𝒫 𝑇𝑋𝑇)
1413biimpri 218 . . . 4 (𝑋𝑇𝑋 ∈ 𝒫 𝑇)
1514adantl 482 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇) → 𝑋 ∈ 𝒫 𝑇)
16 fvex 6158 . . 3 (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊)) ∈ V
17 sseq1 3605 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥𝑧𝑋𝑧))
1817rabbidv 3177 . . . . . . . . . 10 (𝑥 = 𝑋 → {𝑧 ∈ ran 𝐼𝑥𝑧} = {𝑧 ∈ ran 𝐼𝑋𝑧})
1918inteqd 4445 . . . . . . . . 9 (𝑥 = 𝑋 {𝑧 ∈ ran 𝐼𝑥𝑧} = {𝑧 ∈ ran 𝐼𝑋𝑧})
2019fveq2d 6152 . . . . . . . 8 (𝑥 = 𝑋 → (𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧}) = (𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧}))
2120fveq2d 6152 . . . . . . 7 (𝑥 = 𝑋 → ( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) = ( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})))
2221oveq1d 6619 . . . . . 6 (𝑥 = 𝑋 → (( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) = (( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)))
2322oveq1d 6619 . . . . 5 (𝑥 = 𝑋 → ((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊) = ((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊))
2423fveq2d 6152 . . . 4 (𝑥 = 𝑋 → (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊)) = (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊)))
25 eqid 2621 . . . 4 (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊))) = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊)))
2624, 25fvmptg 6237 . . 3 ((𝑋 ∈ 𝒫 𝑇 ∧ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊)) ∈ V) → ((𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊)))‘𝑋) = (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊)))
2715, 16, 26sylancl 693 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇) → ((𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑥𝑧})) ( 𝑊)) 𝑊)))‘𝑋) = (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊)))
2810, 27eqtrd 2655 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇) → (𝑁𝑋) = (𝐼‘((( ‘(𝐼 {𝑧 ∈ ran 𝐼𝑋𝑧})) ( 𝑊)) 𝑊)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  {crab 2911  Vcvv 3186  wss 3555  𝒫 cpw 4130   cint 4440  cmpt 4673  ccnv 5073  ran crn 5075  cfv 5847  (class class class)co 6604  occoc 15870  joincjn 16865  meetcmee 16866  HLchlt 34114  LHypclh 34747  LTrncltrn 34864  DIsoAcdia 35794  ocAcocaN 35885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-docaN 35886
This theorem is referenced by:  docaclN  35890  diaocN  35891
  Copyright terms: Public domain W3C validator