Theorem isphl 19195

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 5875	. . . . 5 |- ( Base ` g ) e. _V
2	1	a1i 11	. . . 4 |- ( g = W -> ( Base ` g ) e. _V )
3		fvex 5875	. . . . . 6 |- ( .i ` g ) e. _V
4	3	a1i 11	. . . . 5 |- ( ( g = W /\ v = ( Base ` g ) ) -> ( .i ` g ) e. _V )
5		fvex 5875	. . . . . . 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 760	. . . . . . . . . . 11 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> g = W )
9	8	fveq2d 5869	. . . . . . . . . 10 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = (Scalar ` W ) )
10		isphl.f	. . . . . . . . . 10 |- F = (Scalar ` W )
11	9, 10	syl6eqr 2503	. . . . . . . . 9 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = F )
12	7, 11	sylan9eqr 2507	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> f = F )
13	12	eleq1d 2513	. . . . . . 7 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( f e. *Ring <-> F e. *Ring ) )
14		simpllr 769	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> v = ( Base ` g ) )
15		simplll 768	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> g = W )
16	15	fveq2d 5869	. . . . . . . . . 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 2503	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( Base ` g ) = V )
19	14, 18	eqtrd 2485	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> v = V )
20		simplr 762	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> h = ( .i ` g ) )
21	15	fveq2d 5869	. . . . . . . . . . . . . 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 2503	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( .i ` g ) = ., )
24	20, 23	eqtrd 2485	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> h = ., )
25	24	oveqd 6307	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( y h x ) = ( y ., x ) )
26	19, 25	mpteq12dv 4481	. . . . . . . . . 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 5869	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> (ringLMod ` f ) = (ringLMod ` F ) )
28	15, 27	oveq12d 6308	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( g LMHom (ringLMod ` f ) ) = ( W LMHom (ringLMod ` F ) ) )
29	26, 28	eleq12d 2523	. . . . . . . . 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 6307	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h x ) = ( x ., x ) )
31	12	fveq2d 5869	. . . . . . . . . . . 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 2503	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` f ) = Z )
34	30, 33	eqeq12d 2466	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( x h x ) = ( 0g ` f ) <-> ( x ., x ) = Z ) )
35	15	fveq2d 5869	. . . . . . . . . . . 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 2503	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` g ) = .0. )
38	37	eqeq2d 2461	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x = ( 0g ` g ) <-> x = .0. ) )
39	34, 38	imbi12d 322	. . . . . . . . 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 5869	. . . . . . . . . . . . 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 2503	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( *r ` f ) = .* )
43	24	oveqd 6307	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h y ) = ( x ., y ) )
44	42, 43	fveq12d 5871	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( *r ` f ) ` ( x h y ) ) = ( .* ` ( x ., y ) ) )
45	44, 25	eqeq12d 2466	. . . . . . . . . 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 3001	. . . . . . . . 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 1339	. . . . . . . 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 3001	. . . . . . 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 717	. . . . . 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 3304	. . . . 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 3304	. . . 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 3304	. . 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 19193	. . 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 3198	. 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 989	. 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 256	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 188   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   A.wral 2737   _Vcvv 3045   [.wsbc 3267   |-> cmpt 4461   ` cfv 5582  (class class class)co 6290   Basecbs 15121   *rcstv 15192  Scalarcsca 15193   .icip 15195   0gc0g 15338   *Ringcsr 18072   LMHom clmhm 18242   LVecclvec 18325  ringLModcrglmod 18392   PreHilcphl 19191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-nul 4534

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-iota 5546  df-fv 5590  df-ov 6293  df-phl 19193

This theorem is referenced by:  phllvec  19196  phlsrng  19198  phllmhm  19199  ipcj  19201  ipeq0  19205  isphld  19221  phlpropd  19222