Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dochsatshpb Unicode version

Theorem dochsatshpb 35378
 Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.)
Hypotheses
Ref Expression
dochsatshpb.h
dochsatshpb.o
dochsatshpb.u
dochsatshpb.s
dochsatshpb.a
dochsatshpb.y
dochsatshpb.k
dochsatshpb.q
Assertion
Ref Expression
dochsatshpb

Proof of Theorem dochsatshpb
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dochsatshpb.h . . 3
2 dochsatshpb.u . . 3
3 dochsatshpb.o . . 3
4 dochsatshpb.a . . 3
5 dochsatshpb.y . . 3
6 dochsatshpb.k . . . 4
8 simpr 461 . . 3
91, 2, 3, 4, 5, 7, 8dochsatshp 35377 . 2
10 dochsatshpb.q . . . . . . . . . . 11
11 eqid 2450 . . . . . . . . . . . 12
12 dochsatshpb.s . . . . . . . . . . . 12
1311, 12lssss 17108 . . . . . . . . . . 11
1410, 13syl 16 . . . . . . . . . 10
15 eqid 2450 . . . . . . . . . . 11
161, 15, 2, 11, 3dochcl 35279 . . . . . . . . . 10
176, 14, 16syl2anc 661 . . . . . . . . 9
181, 15, 3dochoc 35293 . . . . . . . . 9
196, 17, 18syl2anc 661 . . . . . . . 8
2019adantr 465 . . . . . . 7
211, 2, 6dvhlmod 35036 . . . . . . . . 9
2221adantr 465 . . . . . . . 8
23 simpr 461 . . . . . . . 8
2411, 5, 22, 23lshpne 32908 . . . . . . 7
2520, 24eqnetrd 2738 . . . . . 6
26 eqid 2450 . . . . . . . 8
271, 2, 11, 3dochssv 35281 . . . . . . . . 9
286, 14, 27syl2anc 661 . . . . . . . 8
291, 3, 2, 11, 26, 6, 28dochn0nv 35301 . . . . . . 7
3029adantr 465 . . . . . 6
3125, 30mpbird 232 . . . . 5
321, 2, 11, 12, 3dochlss 35280 . . . . . . . . . 10
336, 14, 32syl2anc 661 . . . . . . . . 9
3411, 12lssss 17108 . . . . . . . . 9
3533, 34syl 16 . . . . . . . 8
361, 2, 11, 12, 3dochlss 35280 . . . . . . . 8
376, 35, 36syl2anc 661 . . . . . . 7
3837adantr 465 . . . . . 6
3926, 12lssne0 17122 . . . . . 6
4038, 39syl 16 . . . . 5
4131, 40mpbid 210 . . . 4
426adantr 465 . . . . . . . . . . . 12
43423ad2ant1 1009 . . . . . . . . . . 11
4417adantr 465 . . . . . . . . . . . 12
45443ad2ant1 1009 . . . . . . . . . . 11
4643, 45, 18syl2anc 661 . . . . . . . . . 10
47 eqid 2450 . . . . . . . . . . . 12
48223ad2ant1 1009 . . . . . . . . . . . 12
49383ad2ant1 1009 . . . . . . . . . . . 12
50 simp2 989 . . . . . . . . . . . 12
5112, 47, 48, 49, 50lspsnel5a 17167 . . . . . . . . . . 11
5211, 12lssel 17109 . . . . . . . . . . . . . 14
5349, 50, 52syl2anc 661 . . . . . . . . . . . . 13
541, 2, 11, 47, 15dihlsprn 35257 . . . . . . . . . . . . 13
5543, 53, 54syl2anc 661 . . . . . . . . . . . 12
561, 15, 2, 11, 3dochcl 35279 . . . . . . . . . . . . . . 15
576, 35, 56syl2anc 661 . . . . . . . . . . . . . 14
5857adantr 465 . . . . . . . . . . . . 13
59583ad2ant1 1009 . . . . . . . . . . . 12
601, 15, 3, 43, 55, 59dochord 35296 . . . . . . . . . . 11
6151, 60mpbid 210 . . . . . . . . . 10
6246, 61eqsstr3d 3473 . . . . . . . . 9
631, 2, 6dvhlvec 35035 . . . . . . . . . . . 12
6463adantr 465 . . . . . . . . . . 11
65643ad2ant1 1009 . . . . . . . . . 10
66 simp1r 1013 . . . . . . . . . 10
67 simp3 990 . . . . . . . . . . . 12
6811, 47, 26, 4lsatlspsn2 32918 . . . . . . . . . . . 12
6948, 53, 67, 68syl3anc 1219 . . . . . . . . . . 11
701, 2, 3, 4, 5, 43, 69dochsatshp 35377 . . . . . . . . . 10
715, 65, 66, 70lshpcmp 32914 . . . . . . . . 9
7262, 71mpbid 210 . . . . . . . 8
7372fveq2d 5777 . . . . . . 7
741, 15, 3dochoc 35293 . . . . . . . 8
7543, 55, 74syl2anc 661 . . . . . . 7
7673, 75eqtrd 2490 . . . . . 6
7776, 69eqeltrd 2536 . . . . 5
7877rexlimdv3a 2923 . . . 4
7941, 78mpd 15 . . 3
8010adantr 465 . . . 4
811, 3, 2, 12, 4, 42, 80dochsat 35309 . . 3
8279, 81mpbid 210 . 2
839, 82impbida 828 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1757  =/=wne 2641  E.wrex 2793  C_wss 3410  {csn 3959  rancrn 4923  `cfv 5500   cbs 14260   c0g 14464   clmod 17038   clss 17103   clspn 17142   clvec 17273   clsa 32900   clsh 32901   chlt 33276   clh 33909   cdvh 35004   cdih 35154   coch 35273 This theorem is referenced by:  dochshpsat  35380  dochkrsat  35381  lcfl4N  35421 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-cnex 9423  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443  ax-pre-mulgt0 9444  ax-riotaBAD 32885 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-int 4211  df-iun 4255  df-iin 4256  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-om 6561  df-1st 6661  df-2nd 6662  df-tpos 6829  df-undef 6876  df-recs 6916  df-rdg 6950  df-1o 7004  df-oadd 7008  df-er 7185  df-map 7300  df-en 7395  df-dom 7396  df-sdom 7397  df-fin 7398  df-pnf 9505  df-mnf 9506  df-xr 9507  df-ltxr 9508  df-le 9509  df-sub 9682  df-neg 9683  df-nn 10408  df-2 10465  df-3 10466  df-4 10467  df-5 10468  df-6 10469  df-n0 10665  df-z 10732  df-uz 10947  df-fz 11523  df-struct 14262  df-ndx 14263  df-slot 14264  df-base 14265  df-sets 14266  df-ress 14267  df-plusg 14337  df-mulr 14338  df-sca 14340  df-vsca 14341  df-0g 14466  df-poset 15202  df-plt 15214  df-lub 15230  df-glb 15231  df-join 15232  df-meet 15233  df-p0 15295  df-p1 15296  df-lat 15302  df-clat 15364  df-mnd 15501  df-submnd 15551  df-grp 15631  df-minusg 15632  df-sbg 15633  df-subg 15764  df-cntz 15921  df-lsm 16223  df-cmn 16367  df-abl 16368  df-mgp 16681  df-ur 16693  df-rng 16737  df-oppr 16805  df-dvdsr 16823  df-unit 16824  df-invr 16854  df-dvr 16865  df-drng 16924  df-lmod 17040  df-lss 17104  df-lsp 17143  df-lvec 17274  df-lsatoms 32902  df-lshyp 32903  df-oposet 33102  df-ol 33104  df-oml 33105  df-covers 33192  df-ats 33193  df-atl 33224  df-cvlat 33248  df-hlat 33277  df-llines 33423  df-lplanes 33424  df-lvols 33425  df-lines 33426  df-psubsp 33428  df-pmap 33429  df-padd 33721  df-lhyp 33913  df-laut 33914  df-ldil 34029  df-ltrn 34030  df-trl 34084  df-tgrp 34668  df-tendo 34680  df-edring 34682  df-dveca 34928  df-disoa 34955  df-dvech 35005  df-dib 35065  df-dic 35099  df-dih 35155  df-doch 35274  df-djh 35321
 Copyright terms: Public domain W3C validator