Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ocvlss Unicode version

Theorem ocvlss 16840
 Description: The orthocomplement of a subset is a linear subspace of the pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015.)
Hypotheses
Ref Expression
ocvss.v
ocvss.o
ocvlss.l
Assertion
Ref Expression
ocvlss

Proof of Theorem ocvlss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ocvss.v . . . 4
2 ocvss.o . . . 4
31, 2ocvss 16838 . . 3
43a1i 11 . 2
5 simpr 448 . . . 4
6 phllmod 16802 . . . . . 6
76adantr 452 . . . . 5
8 eqid 2401 . . . . . 6
91, 8lmod0vcl 15920 . . . . 5
107, 9syl 16 . . . 4
11 simpll 731 . . . . . 6
125sselda 3305 . . . . . 6
13 eqid 2401 . . . . . . 7 Scalar Scalar
14 eqid 2401 . . . . . . 7
15 eqid 2401 . . . . . . 7 Scalar Scalar
1613, 14, 1, 15, 8ip0l 16808 . . . . . 6 Scalar
1711, 12, 16syl2anc 643 . . . . 5 Scalar
1817ralrimiva 2746 . . . 4 Scalar
191, 14, 13, 15, 2elocv 16836 . . . 4 Scalar
205, 10, 18, 19syl3anbrc 1138 . . 3
21 ne0i 3591 . . 3
2220, 21syl 16 . 2
235adantr 452 . . . 4 Scalar
247adantr 452 . . . . 5 Scalar
25 simpr1 963 . . . . . 6 Scalar Scalar
26 simpr2 964 . . . . . . 7 Scalar
273, 26sseldi 3303 . . . . . 6 Scalar
28 eqid 2401 . . . . . . 7
29 eqid 2401 . . . . . . 7 Scalar Scalar
301, 13, 28, 29lmodvscl 15908 . . . . . 6 Scalar
3124, 25, 27, 30syl3anc 1184 . . . . 5 Scalar
32 simpr3 965 . . . . . 6 Scalar
333, 32sseldi 3303 . . . . 5 Scalar
34 eqid 2401 . . . . . 6
351, 34lmodvacl 15905 . . . . 5
3624, 31, 33, 35syl3anc 1184 . . . 4 Scalar
3711adantlr 696 . . . . . . 7 Scalar
3831adantr 452 . . . . . . 7 Scalar
3933adantr 452 . . . . . . 7 Scalar
4012adantlr 696 . . . . . . 7 Scalar
41 eqid 2401 . . . . . . . 8 Scalar Scalar
4213, 14, 1, 34, 41ipdir 16811 . . . . . . 7 Scalar
4337, 38, 39, 40, 42syl13anc 1186 . . . . . 6 Scalar Scalar
4425adantr 452 . . . . . . . . 9 Scalar Scalar
4527adantr 452 . . . . . . . . 9 Scalar
46 eqid 2401 . . . . . . . . . 10 Scalar Scalar
4713, 14, 1, 29, 28, 46ipass 16817 . . . . . . . . 9 Scalar Scalar
4837, 44, 45, 40, 47syl13anc 1186 . . . . . . . 8 Scalar Scalar
491, 14, 13, 15, 2ocvi 16837 . . . . . . . . . 10 Scalar
5026, 49sylan 458 . . . . . . . . 9 Scalar Scalar
5150oveq2d 6050 . . . . . . . 8 Scalar Scalar ScalarScalar
5224adantr 452 . . . . . . . . . 10 Scalar
5313lmodrng 15899 . . . . . . . . . 10 Scalar
5452, 53syl 16 . . . . . . . . 9 Scalar Scalar
5529, 46, 15rngrz 15642 . . . . . . . . 9 Scalar Scalar ScalarScalar Scalar
5654, 44, 55syl2anc 643 . . . . . . . 8 Scalar ScalarScalar Scalar
5748, 51, 563eqtrd 2437 . . . . . . 7 Scalar Scalar
581, 14, 13, 15, 2ocvi 16837 . . . . . . . 8 Scalar
5932, 58sylan 458 . . . . . . 7 Scalar Scalar
6057, 59oveq12d 6052 . . . . . 6 Scalar Scalar Scalar ScalarScalar
6113lmodfgrp 15900 . . . . . . 7 Scalar
6229, 15grpidcl 14774 . . . . . . . 8 Scalar Scalar Scalar
6329, 41, 15grplid 14776 . . . . . . . 8 Scalar Scalar Scalar Scalar ScalarScalar Scalar
6462, 63mpdan 650 . . . . . . 7 Scalar Scalar ScalarScalar Scalar
6552, 61, 643syl 19 . . . . . 6 Scalar Scalar ScalarScalar Scalar
6643, 60, 653eqtrd 2437 . . . . 5 Scalar Scalar
6766ralrimiva 2746 . . . 4 Scalar Scalar
681, 14, 13, 15, 2elocv 16836 . . . 4 Scalar
6923, 36, 67, 68syl3anbrc 1138 . . 3 Scalar
7069ralrimivvva 2756 . 2 Scalar
71 ocvlss.l . . 3
7213, 29, 1, 34, 28, 71islss 15952 . 2 Scalar
734, 22, 70, 72syl3anbrc 1138 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2564  wral 2663   wss 3277  c0 3585  cfv 5408  (class class class)co 6034  cbs 13410   cplusg 13470  cmulr 13471  Scalarcsca 13473  cvsca 13474  cip 13475  c0g 13664  cgrp 14626  crg 15601  clmod 15891  clss 15949  cphl 16796  cocv 16828 This theorem is referenced by:  ocvin  16842  ocvlsp  16844  csslss  16859  pjdm2  16879  pjff  16880  pjf2  16882  pjfo  16883  ocvpj  16885  pjthlem2  19278  pjth  19279 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-riota 6499  df-recs 6583  df-rdg 6618  df-er 6855  df-en 7060  df-dom 7061  df-sdom 7062  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-plusg 13483  df-sca 13486  df-vsca 13487  df-0g 13668  df-mnd 14631  df-grp 14753  df-ghm 14945  df-mgp 15590  df-rng 15604  df-lmod 15893  df-lss 15950  df-lmhm 16039  df-lvec 16116  df-sra 16185  df-rgmod 16186  df-phl 16798  df-ocv 16831
 Copyright terms: Public domain W3C validator