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

Theorem isobs 20478
 Description: The predicate "is an orthonormal basis" (over a pre-Hilbert space). (Contributed by Mario Carneiro, 23-Oct-2015.)
Hypotheses
Ref Expression
isobs.v 𝑉 = (Base‘𝑊)
isobs.h , = (·𝑖𝑊)
isobs.f 𝐹 = (Scalar‘𝑊)
isobs.u 1 = (1r𝐹)
isobs.z 0 = (0g𝐹)
isobs.o = (ocv‘𝑊)
isobs.y 𝑌 = (0g𝑊)
Assertion
Ref Expression
isobs (𝐵 ∈ (OBasis‘𝑊) ↔ (𝑊 ∈ PreHil ∧ 𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})))
Distinct variable groups:   𝑥,𝑦, ,   𝑥, 0 ,𝑦   𝑥, 1 ,𝑦   𝑥,𝐵,𝑦   𝑥,𝑊,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)   (𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem isobs
Dummy variables 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-obs 20463 . . . 4 OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
21mptrcl 6769 . . 3 (𝐵 ∈ (OBasis‘𝑊) → 𝑊 ∈ PreHil)
3 fveq2 6659 . . . . . . . . 9 ( = 𝑊 → (Base‘) = (Base‘𝑊))
4 isobs.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
53, 4eqtr4di 2812 . . . . . . . 8 ( = 𝑊 → (Base‘) = 𝑉)
65pweqd 4514 . . . . . . 7 ( = 𝑊 → 𝒫 (Base‘) = 𝒫 𝑉)
7 fveq2 6659 . . . . . . . . . . . 12 ( = 𝑊 → (·𝑖) = (·𝑖𝑊))
8 isobs.h . . . . . . . . . . . 12 , = (·𝑖𝑊)
97, 8eqtr4di 2812 . . . . . . . . . . 11 ( = 𝑊 → (·𝑖) = , )
109oveqd 7168 . . . . . . . . . 10 ( = 𝑊 → (𝑥(·𝑖)𝑦) = (𝑥 , 𝑦))
11 fveq2 6659 . . . . . . . . . . . . . 14 ( = 𝑊 → (Scalar‘) = (Scalar‘𝑊))
12 isobs.f . . . . . . . . . . . . . 14 𝐹 = (Scalar‘𝑊)
1311, 12eqtr4di 2812 . . . . . . . . . . . . 13 ( = 𝑊 → (Scalar‘) = 𝐹)
1413fveq2d 6663 . . . . . . . . . . . 12 ( = 𝑊 → (1r‘(Scalar‘)) = (1r𝐹))
15 isobs.u . . . . . . . . . . . 12 1 = (1r𝐹)
1614, 15eqtr4di 2812 . . . . . . . . . . 11 ( = 𝑊 → (1r‘(Scalar‘)) = 1 )
1713fveq2d 6663 . . . . . . . . . . . 12 ( = 𝑊 → (0g‘(Scalar‘)) = (0g𝐹))
18 isobs.z . . . . . . . . . . . 12 0 = (0g𝐹)
1917, 18eqtr4di 2812 . . . . . . . . . . 11 ( = 𝑊 → (0g‘(Scalar‘)) = 0 )
2016, 19ifeq12d 4442 . . . . . . . . . 10 ( = 𝑊 → if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) = if(𝑥 = 𝑦, 1 , 0 ))
2110, 20eqeq12d 2775 . . . . . . . . 9 ( = 𝑊 → ((𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ↔ (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 )))
22212ralbidv 3129 . . . . . . . 8 ( = 𝑊 → (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ↔ ∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 )))
23 fveq2 6659 . . . . . . . . . . 11 ( = 𝑊 → (ocv‘) = (ocv‘𝑊))
24 isobs.o . . . . . . . . . . 11 = (ocv‘𝑊)
2523, 24eqtr4di 2812 . . . . . . . . . 10 ( = 𝑊 → (ocv‘) = )
2625fveq1d 6661 . . . . . . . . 9 ( = 𝑊 → ((ocv‘)‘𝑏) = ( 𝑏))
27 fveq2 6659 . . . . . . . . . . 11 ( = 𝑊 → (0g) = (0g𝑊))
28 isobs.y . . . . . . . . . . 11 𝑌 = (0g𝑊)
2927, 28eqtr4di 2812 . . . . . . . . . 10 ( = 𝑊 → (0g) = 𝑌)
3029sneqd 4535 . . . . . . . . 9 ( = 𝑊 → {(0g)} = {𝑌})
3126, 30eqeq12d 2775 . . . . . . . 8 ( = 𝑊 → (((ocv‘)‘𝑏) = {(0g)} ↔ ( 𝑏) = {𝑌}))
3222, 31anbi12d 634 . . . . . . 7 ( = 𝑊 → ((∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)}) ↔ (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌})))
336, 32rabeqbidv 3399 . . . . . 6 ( = 𝑊 → {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})} = {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌})})
344fvexi 6673 . . . . . . . 8 𝑉 ∈ V
3534pwex 5250 . . . . . . 7 𝒫 𝑉 ∈ V
3635rabex 5203 . . . . . 6 {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌})} ∈ V
3733, 1, 36fvmpt 6760 . . . . 5 (𝑊 ∈ PreHil → (OBasis‘𝑊) = {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌})})
3837eleq2d 2838 . . . 4 (𝑊 ∈ PreHil → (𝐵 ∈ (OBasis‘𝑊) ↔ 𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌})}))
39 raleq 3324 . . . . . . . 8 (𝑏 = 𝐵 → (∀𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ↔ ∀𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 )))
4039raleqbi1dv 3322 . . . . . . 7 (𝑏 = 𝐵 → (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ↔ ∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 )))
41 fveqeq2 6668 . . . . . . 7 (𝑏 = 𝐵 → (( 𝑏) = {𝑌} ↔ ( 𝐵) = {𝑌}))
4240, 41anbi12d 634 . . . . . 6 (𝑏 = 𝐵 → ((∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌}) ↔ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})))
4342elrab 3603 . . . . 5 (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌})} ↔ (𝐵 ∈ 𝒫 𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})))
4434elpw2 5216 . . . . . 6 (𝐵 ∈ 𝒫 𝑉𝐵𝑉)
4544anbi1i 627 . . . . 5 ((𝐵 ∈ 𝒫 𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})) ↔ (𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})))
4643, 45bitri 278 . . . 4 (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥𝑏𝑦𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝑏) = {𝑌})} ↔ (𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})))
4738, 46bitrdi 290 . . 3 (𝑊 ∈ PreHil → (𝐵 ∈ (OBasis‘𝑊) ↔ (𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌}))))
482, 47biadanii 822 . 2 (𝐵 ∈ (OBasis‘𝑊) ↔ (𝑊 ∈ PreHil ∧ (𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌}))))
49 3anass 1093 . 2 ((𝑊 ∈ PreHil ∧ 𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})) ↔ (𝑊 ∈ PreHil ∧ (𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌}))))
5048, 49bitr4i 281 1 (𝐵 ∈ (OBasis‘𝑊) ↔ (𝑊 ∈ PreHil ∧ 𝐵𝑉 ∧ (∀𝑥𝐵𝑦𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( 𝐵) = {𝑌})))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∀wral 3071  {crab 3075   ⊆ wss 3859  ifcif 4421  𝒫 cpw 4495  {csn 4523  ‘cfv 6336  (class class class)co 7151  Basecbs 16534  Scalarcsca 16619  ·𝑖cip 16621  0gc0g 16764  1rcur 19312  PreHilcphl 20382  ocvcocv 20418  OBasiscobs 20460 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7154  df-obs 20463 This theorem is referenced by:  obsip  20479  obsrcl  20481  obsss  20482  obsocv  20484
 Copyright terms: Public domain W3C validator