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

Theorem isobs 19220
 Description: The predicate "is an orthonormal basis" (over a pre-Hilbert space). (Contributed by Mario Carneiro, 23-Oct-2015.)
Hypotheses
Ref Expression
isobs.v
isobs.h
isobs.f Scalar
isobs.u
isobs.z
isobs.o
isobs.y
Assertion
Ref Expression
isobs OBasis
Distinct variable groups:   ,,   , ,   , ,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)

Proof of Theorem isobs
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-obs 19205 . . . . 5 OBasis Scalar Scalar
21dmmptss 5288 . . . 4 OBasis
3 elfvdm 5846 . . . 4 OBasis OBasis
42, 3sseldi 3400 . . 3 OBasis
5 fveq2 5820 . . . . . . . . 9
6 isobs.v . . . . . . . . 9
75, 6syl6eqr 2475 . . . . . . . 8
87pweqd 3924 . . . . . . 7
9 fveq2 5820 . . . . . . . . . . . 12
10 isobs.h . . . . . . . . . . . 12
119, 10syl6eqr 2475 . . . . . . . . . . 11
1211oveqd 6261 . . . . . . . . . 10
13 fveq2 5820 . . . . . . . . . . . . . 14 Scalar Scalar
14 isobs.f . . . . . . . . . . . . . 14 Scalar
1513, 14syl6eqr 2475 . . . . . . . . . . . . 13 Scalar
1615fveq2d 5824 . . . . . . . . . . . 12 Scalar
17 isobs.u . . . . . . . . . . . 12
1816, 17syl6eqr 2475 . . . . . . . . . . 11 Scalar
1915fveq2d 5824 . . . . . . . . . . . 12 Scalar
20 isobs.z . . . . . . . . . . . 12
2119, 20syl6eqr 2475 . . . . . . . . . . 11 Scalar
2218, 21ifeq12d 3869 . . . . . . . . . 10 Scalar Scalar
2312, 22eqeq12d 2438 . . . . . . . . 9 Scalar Scalar
24232ralbidv 2804 . . . . . . . 8 Scalar Scalar
25 fveq2 5820 . . . . . . . . . . 11
26 isobs.o . . . . . . . . . . 11
2725, 26syl6eqr 2475 . . . . . . . . . 10
2827fveq1d 5822 . . . . . . . . 9
29 fveq2 5820 . . . . . . . . . . 11
30 isobs.y . . . . . . . . . . 11
3129, 30syl6eqr 2475 . . . . . . . . . 10
3231sneqd 3948 . . . . . . . . 9
3328, 32eqeq12d 2438 . . . . . . . 8
3424, 33anbi12d 715 . . . . . . 7 Scalar Scalar
358, 34rabeqbidv 3012 . . . . . 6 Scalar Scalar
36 fvex 5830 . . . . . . . . 9
376, 36eqeltri 2497 . . . . . . . 8
3837pwex 4545 . . . . . . 7
3938rabex 4513 . . . . . 6
4035, 1, 39fvmpt 5903 . . . . 5 OBasis
4140eleq2d 2486 . . . 4 OBasis
42 raleq 2959 . . . . . . . 8
4342raleqbi1dv 2967 . . . . . . 7
44 fveq2 5820 . . . . . . . 8
4544eqeq1d 2425 . . . . . . 7
4643, 45anbi12d 715 . . . . . 6
4746elrab 3166 . . . . 5
4837elpw2 4526 . . . . . 6
4948anbi1i 699 . . . . 5
5047, 49bitri 252 . . . 4
5141, 50syl6bb 264 . . 3 OBasis
524, 51biadan2 646 . 2 OBasis
53 3anass 986 . 2
5452, 53bitr4i 255 1 OBasis
 Colors of variables: wff setvar class Syntax hints:   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  wral 2709  crab 2713  cvv 3017   wss 3374  cif 3849  cpw 3919  csn 3936   cdm 4791  cfv 5539  (class class class)co 6244  cbs 15059  Scalarcsca 15131  cip 15133  c0g 15276  cur 17673  cphl 19128  cocv 19160  OBasiscobs 19202 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fv 5547  df-ov 6247  df-obs 19205 This theorem is referenced by:  obsip  19221  obsrcl  19223  obsss  19224  obsocv  19226
 Copyright terms: Public domain W3C validator