Theorem isphl 18079

Description: The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2015.)

Hypotheses

Ref	Expression
isphl.v	|- V = ( Base ` W )
isphl.f	|- F = (Scalar ` W )
isphl.h	|- ., = ( .i ` W )
isphl.o	|- .0. = ( 0g ` W )
isphl.i	|- .* = ( *r ` F )
isphl.z	|- Z = ( 0g ` F )

Assertion

Ref	Expression
isphl	|- ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )

Distinct variable groups:   x, y, V   x, W, y

Allowed substitution hints:   F( x, y)   ., ( x, y)   .* ( x, y)   .0. ( x, y)   Z( x, y)

Proof of Theorem isphl

Dummy variables f g h v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 5722	. . . . 5 |- ( Base ` g ) e. _V
2	1	a1i 11	. . . 4 |- ( g = W -> ( Base ` g ) e. _V )
3		fvex 5722	. . . . . 6 |- ( .i ` g ) e. _V
4	3	a1i 11	. . . . 5 |- ( ( g = W /\ v = ( Base ` g ) ) -> ( .i ` g ) e. _V )
5		fvex 5722	. . . . . . 7 |- (Scalar ` g ) e. _V
6	5	a1i 11	. . . . . 6 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) e. _V )
7		id 22	. . . . . . . . 9 |- ( f = (Scalar ` g ) -> f = (Scalar ` g ) )
8		simpll 753	. . . . . . . . . . 11 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> g = W )
9	8	fveq2d 5716	. . . . . . . . . 10 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = (Scalar ` W ) )
10		isphl.f	. . . . . . . . . 10 |- F = (Scalar ` W )
11	9, 10	syl6eqr 2493	. . . . . . . . 9 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = F )
12	7, 11	sylan9eqr 2497	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> f = F )
13	12	eleq1d 2509	. . . . . . 7 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( f e. *Ring <-> F e. *Ring ) )
14		simpllr 758	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> v = ( Base ` g ) )
15		simplll 757	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> g = W )
16	15	fveq2d 5716	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( Base ` g ) = ( Base ` W ) )
17		isphl.v	. . . . . . . . . 10 |- V = ( Base ` W )
18	16, 17	syl6eqr 2493	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( Base ` g ) = V )
19	14, 18	eqtrd 2475	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> v = V )
20		simplr 754	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> h = ( .i ` g ) )
21	15	fveq2d 5716	. . . . . . . . . . . . . 14 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( .i ` g ) = ( .i ` W ) )
22		isphl.h	. . . . . . . . . . . . . 14 |- ., = ( .i ` W )
23	21, 22	syl6eqr 2493	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( .i ` g ) = ., )
24	20, 23	eqtrd 2475	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> h = ., )
25	24	oveqd 6129	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( y h x ) = ( y ., x ) )
26	19, 25	mpteq12dv 4391	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( y e. v |-> ( y h x ) ) = ( y e. V |-> ( y ., x ) ) )
27	12	fveq2d 5716	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> (ringLMod ` f ) = (ringLMod ` F ) )
28	15, 27	oveq12d 6130	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( g LMHom (ringLMod ` f ) ) = ( W LMHom (ringLMod ` F ) ) )
29	26, 28	eleq12d 2511	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) <-> ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) ) )
30	24	oveqd 6129	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h x ) = ( x ., x ) )
31	12	fveq2d 5716	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` f ) = ( 0g ` F ) )
32		isphl.z	. . . . . . . . . . . 12 |- Z = ( 0g ` F )
33	31, 32	syl6eqr 2493	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` f ) = Z )
34	30, 33	eqeq12d 2457	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( x h x ) = ( 0g ` f ) <-> ( x ., x ) = Z ) )
35	15	fveq2d 5716	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` g ) = ( 0g ` W ) )
36		isphl.o	. . . . . . . . . . . 12 |- .0. = ( 0g ` W )
37	35, 36	syl6eqr 2493	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` g ) = .0. )
38	37	eqeq2d 2454	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x = ( 0g ` g ) <-> x = .0. ) )
39	34, 38	imbi12d 320	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) <-> ( ( x ., x ) = Z -> x = .0. ) ) )
40	12	fveq2d 5716	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( *r ` f ) = ( *r ` F ) )
41		isphl.i	. . . . . . . . . . . . 13 |- .* = ( *r ` F )
42	40, 41	syl6eqr 2493	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( *r ` f ) = .* )
43	24	oveqd 6129	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h y ) = ( x ., y ) )
44	42, 43	fveq12d 5718	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( *r ` f ) ` ( x h y ) ) = ( .* ` ( x ., y ) ) )
45	44, 25	eqeq12d 2457	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) <-> ( .* ` ( x ., y ) ) = ( y ., x ) ) )
46	19, 45	raleqbidv 2952	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) <-> A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) )
47	29, 39, 46	3anbi123d 1289	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) <-> ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )
48	19, 47	raleqbidv 2952	. . . . . . 7 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) <-> A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )
49	13, 48	anbi12d 710	. . . . . 6 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
50	6, 49	sbcied 3244	. . . . 5 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> ( [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
51	4, 50	sbcied 3244	. . . 4 |- ( ( g = W /\ v = ( Base ` g ) ) -> ( [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
52	2, 51	sbcied 3244	. . 3 |- ( g = W -> ( [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
53		df-phl 18077	. . 3 |- PreHil = { g e. LVec | [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) }
54	52, 53	elrab2 3140	. 2 |- ( W e. PreHil <-> ( W e. LVec /\ ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
55		3anass 969	. 2 |- ( ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) <-> ( W e. LVec /\ ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
56	54, 55	bitr4i 252	1 |- ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom (ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   A.wral 2736   _Vcvv 2993   [.wsbc 3207   e. cmpt 4371   ` cfv 5439  (class class class)co 6112   Basecbs 14195   *rcstv 14261  Scalarcsca 14262   .icip 14264   0gc0g 14399   *Ringcsr 16951   LMHom clmhm 17122   LVecclvec 17205  ringLModcrglmod 17272   PreHilcphl 18075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4442

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-iota 5402  df-fv 5447  df-ov 6115  df-phl 18077

This theorem is referenced by:  phllvec  18080  phlsrng  18082  phllmhm  18083  ipcj  18085  ipeq0  18089  isphld  18105  phlpropd  18106