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

Theorem isphld 17791
Description: Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 7-Oct-2015.)
Hypotheses
Ref Expression
isphld.v
isphld.a
isphld.s
isphld.i
isphld.z
isphld.f
isphld.k
isphld.p
isphld.t
isphld.c
isphld.o
isphld.l
isphld.r
isphld.cl
isphld.d
isphld.ns
isphld.cj
Assertion
Ref Expression
isphld
Distinct variable groups:   , , , ,   , , , ,

Proof of Theorem isphld
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 isphld.l . 2
2 isphld.f . . 3
3 isphld.r . . 3
42, 3eqeltrrd 2497 . 2
5 oveq1 6068 . . . . . 6
65cbvmptv 4358 . . . . 5
7 isphld.cl . . . . . . . . . . . . . . 15
873expib 1175 . . . . . . . . . . . . . 14
9 isphld.v . . . . . . . . . . . . . . . 16
109eleq2d 2489 . . . . . . . . . . . . . . 15
119eleq2d 2489 . . . . . . . . . . . . . . 15
1210, 11anbi12d 695 . . . . . . . . . . . . . 14
13 isphld.i . . . . . . . . . . . . . . . 16
1413oveqd 6078 . . . . . . . . . . . . . . 15
15 isphld.k . . . . . . . . . . . . . . . 16
162fveq2d 5665 . . . . . . . . . . . . . . . 16
1715, 16eqtrd 2454 . . . . . . . . . . . . . . 15
1814, 17eleq12d 2490 . . . . . . . . . . . . . 14
198, 12, 183imtr3d 261 . . . . . . . . . . . . 13
2019impl 607 . . . . . . . . . . . 12
2120an32s 787 . . . . . . . . . . 11
22 oveq1 6068 . . . . . . . . . . . 12
2322cbvmptv 4358 . . . . . . . . . . 11
2421, 23fmptd 5837 . . . . . . . . . 10
2524ralrimiva 2778 . . . . . . . . 9
26 oveq2 6069 . . . . . . . . . . . 12
2726mpteq2dv 4354 . . . . . . . . . . 11
2827feq1d 5516 . . . . . . . . . 10
2928rspccva 3050 . . . . . . . . 9
3025, 29sylan 461 . . . . . . . 8
31 eqidd 2423 . . . . . . . 8
32 isphld.d . . . . . . . . . . . . . . . 16
33323exp 1171 . . . . . . . . . . . . . . 15
3417eleq2d 2489 . . . . . . . . . . . . . . 15
35 3anrot 955 . . . . . . . . . . . . . . . . 17
369eleq2d 2489 . . . . . . . . . . . . . . . . . 18
3736, 10, 113anbi123d 1274 . . . . . . . . . . . . . . . . 17
3835, 37syl5bbr 253 . . . . . . . . . . . . . . . 16
39 isphld.a . . . . . . . . . . . . . . . . . . 19
40 isphld.s . . . . . . . . . . . . . . . . . . . 20
4140oveqd 6078 . . . . . . . . . . . . . . . . . . 19
42 eqidd 2423 . . . . . . . . . . . . . . . . . . 19
4339, 41, 42oveq123d 6082 . . . . . . . . . . . . . . . . . 18
44 eqidd 2423 . . . . . . . . . . . . . . . . . 18
4513, 43, 44oveq123d 6082 . . . . . . . . . . . . . . . . 17
46 isphld.p . . . . . . . . . . . . . . . . . . 19
472fveq2d 5665 . . . . . . . . . . . . . . . . . . 19
4846, 47eqtrd 2454 . . . . . . . . . . . . . . . . . 18
49 isphld.t . . . . . . . . . . . . . . . . . . . 20
502fveq2d 5665 . . . . . . . . . . . . . . . . . . . 20
5149, 50eqtrd 2454 . . . . . . . . . . . . . . . . . . 19
52 eqidd 2423 . . . . . . . . . . . . . . . . . . 19
5313oveqd 6078 . . . . . . . . . . . . . . . . . . 19
5451, 52, 53oveq123d 6082 . . . . . . . . . . . . . . . . . 18
5513oveqd 6078 . . . . . . . . . . . . . . . . . 18
5648, 54, 55oveq123d 6082 . . . . . . . . . . . . . . . . 17
5745, 56eqeq12d 2436 . . . . . . . . . . . . . . . 16
5838, 57imbi12d 314 . . . . . . . . . . . . . . 15
5933, 34, 583imtr3d 261 . . . . . . . . . . . . . 14
6059imp31 425 . . . . . . . . . . . . 13
61603exp2 1190 . . . . . . . . . . . 12
6261impancom 431 . . . . . . . . . . 11
63623imp2 1187 . . . . . . . . . 10
64 lveclmod 16996 . . . . . . . . . . . . . . . 16
651, 64syl 16 . . . . . . . . . . . . . . 15
6665adantr 455 . . . . . . . . . . . . . 14
6766adantr 455 . . . . . . . . . . . . 13
68 eqid 2422 . . . . . . . . . . . . . 14
69 eqid 2422 . . . . . . . . . . . . . 14
7068, 69lss1 16829 . . . . . . . . . . . . 13
7167, 70syl 16 . . . . . . . . . . . 12
72 eqid 2422 . . . . . . . . . . . . 13
73 eqid 2422 . . . . . . . . . . . . 13
74 eqid 2422 . . . . . . . . . . . . 13
75 eqid 2422 . . . . . . . . . . . . 13
7672, 73, 74, 75, 69lsscl 16833 . . . . . . . . . . . 12
7771, 76sylancom 652 . . . . . . . . . . 11
78 oveq1 6068 . . . . . . . . . . . 12
79 eqid 2422 . . . . . . . . . . . 12
80 ovex 6086 . . . . . . . . . . . 12
8178, 79, 80fvmpt3i 5748 . . . . . . . . . . 11
8277, 81syl 16 . . . . . . . . . 10
83 simpr2 980 . . . . . . . . . . . . 13
84 oveq1 6068 . . . . . . . . . . . . . 14
8584, 79, 80fvmpt3i 5748 . . . . . . . . . . . . 13
8683, 85syl 16 . . . . . . . . . . . 12
8786oveq2d 6077 . . . . . . . . . . 11
88 simpr3 981 . . . . . . . . . . . 12
89 oveq1 6068 . . . . . . . . . . . . 13
9089, 79, 80fvmpt3i 5748 . . . . . . . . . . . 12
9188, 90syl 16 . . . . . . . . . . 11
9287, 91oveq12d 6079 . . . . . . . . . 10
9363, 82, 923eqtr4d 2464 . . . . . . . . 9
9493ralrimivvva 2788 . . . . . . . 8
9572lmodrng 16769 . . . . . . . . . . 11
96 rlmlmod 17095 . . . . . . . . . . 11
9765, 95, 963syl 19 . . . . . . . . . 10
9897adantr 455 . . . . . . . . 9
99 rlmbas 17085 . . . . . . . . . 10
100 fvex 5671 . . . . . . . . . . 11
101 rlmsca 17090 . . . . . . . . . . 11
102100, 101ax-mp 5 . . . . . . . . . 10
103 rlmplusg 17086 . . . . . . . . . 10
104 rlmvsca 17092 . . . . . . . . . 10
10568, 99, 72, 102, 73, 74, 103, 75, 104islmhm2 16928 . . . . . . . . 9
10666, 98, 105syl2anc 646 . . . . . . . 8
10730, 31, 94, 106mpbir3and 1156 . . . . . . 7
108107ralrimiva 2778 . . . . . 6
109 oveq2 6069 . . . . . . . . 9
110109mpteq2dv 4354 . . . . . . . 8
111110eleq1d 2488 . . . . . . 7
112111rspccva 3050 . . . . . 6
113108, 112sylan 461 . . . . 5
1146, 113syl5eqel 2506 . . . 4
115 isphld.ns . . . . . . 7
1161153exp 1171 . . . . . 6
11713oveqd 6078 . . . . . . . 8
118 isphld.o . . . . . . . . 9
1192fveq2d 5665 . . . . . . . . 9
120118, 119eqtrd 2454 . . . . . . . 8
121117, 120eqeq12d 2436 . . . . . . 7
122 isphld.z . . . . . . . 8
123122eqeq2d 2433 . . . . . . 7
124121, 123imbi12d 314 . . . . . 6
125116, 10, 1243imtr3d 261 . . . . 5
126125imp 422 . . . 4
127 isphld.cj . . . . . . . 8
1281273expib 1175 . . . . . . 7
129 isphld.c . . . . . . . . . 10
1302fveq2d 5665 . . . . . . . . . 10
131129, 130eqtrd 2454 . . . . . . . . 9
132131, 14fveq12d 5667 . . . . . . . 8
13313oveqd 6078 . . . . . . . 8
134132, 133eqeq12d 2436 . . . . . . 7
135128, 12, 1343imtr3d 261 . . . . . 6
136135expdimp 430 . . . . 5
137136ralrimiv 2777 . . . 4
138114, 126, 1373jca 1153 . . 3
139138ralrimiva 2778 . 2
140 eqid 2422 . . 3
141 eqid 2422 . . 3
142 eqid 2422 . . 3
143 eqid 2422 . . 3
14468, 72, 140, 141, 142, 143isphl 17765 . 2
1451, 4, 139, 144syl3anbrc 1157 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  /\wa 362  /\w3a 950  =wceq 1687  e.wcel 1749  A.wral 2694   cvv 2951  e.cmpt 4325  -->wf 5386  `cfv 5390  (class class class)co 6061   cbs 14114   cplusg 14178   cmulr 14179   cstv 14180   csca 14181   cvsca 14182   cip 14183   c0g 14318   crg 16469   csr 16742   clmod 16761   clss 16822   clmhm 16909   clvec 16992   crglmod 17059   cphl 17761
This theorem is referenced by:  frlmphl  17909  hlhilphllem  35044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-cnex 9284  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304  ax-pre-mulgt0 9305
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-tr 4361  df-eprel 4603  df-id 4607  df-po 4612  df-so 4613  df-fr 4650  df-we 4652  df-ord 4693  df-on 4694  df-lim 4695  df-suc 4696  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-om 6447  df-recs 6791  df-rdg 6825  df-er 7062  df-en 7270  df-dom 7271  df-sdom 7272  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-sub 9543  df-neg 9544  df-nn 10269  df-2 10326  df-3 10327  df-4 10328  df-5 10329  df-6 10330  df-7 10331  df-8 10332  df-ndx 14117  df-slot 14118  df-base 14119  df-sets 14120  df-ress 14121  df-plusg 14191  df-mulr 14192  df-sca 14194  df-vsca 14195  df-ip 14196  df-0g 14320  df-mnd 15355  df-grp 15482  df-subg 15615  df-ghm 15682  df-mgp 16458  df-rng 16472  df-ur 16474  df-subrg 16676  df-lmod 16763  df-lss 16823  df-lmhm 16912  df-lvec 16993  df-sra 17062  df-rgmod 17063  df-phl 17763
  Copyright terms: Public domain W3C validator