Theorem isphl 19179

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 5887	. . . . 5 |- ( Base ` g ) e. _V
2	1	a1i 11	. . . 4 |- ( g = W -> ( Base ` g ) e. _V )
3		fvex 5887	. . . . . 6 |- ( .i ` g ) e. _V
4	3	a1i 11	. . . . 5 |- ( ( g = W /\ v = ( Base ` g ) ) -> ( .i ` g ) e. _V )
5		fvex 5887	. . . . . . 7 |- (Scalar ` g ) e. _V
6	5	a1i 11	. . . . . 6 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) e. _V )
7		id 23	. . . . . . . . 9 |- ( f = (Scalar ` g ) -> f = (Scalar ` g ) )
8		simpll 758	. . . . . . . . . . 11 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> g = W )
9	8	fveq2d 5881	. . . . . . . . . 10 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = (Scalar ` W ) )
10		isphl.f	. . . . . . . . . 10 |- F = (Scalar ` W )
11	9, 10	syl6eqr 2481	. . . . . . . . 9 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = F )
12	7, 11	sylan9eqr 2485	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> f = F )
13	12	eleq1d 2491	. . . . . . 7 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( f e. *Ring <-> F e. *Ring ) )
14		simpllr 767	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> v = ( Base ` g ) )
15		simplll 766	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> g = W )
16	15	fveq2d 5881	. . . . . . . . . 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 2481	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( Base ` g ) = V )
19	14, 18	eqtrd 2463	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> v = V )
20		simplr 760	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> h = ( .i ` g ) )
21	15	fveq2d 5881	. . . . . . . . . . . . . 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 2481	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( .i ` g ) = ., )
24	20, 23	eqtrd 2463	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> h = ., )
25	24	oveqd 6318	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( y h x ) = ( y ., x ) )
26	19, 25	mpteq12dv 4499	. . . . . . . . . 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 5881	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> (ringLMod ` f ) = (ringLMod ` F ) )
28	15, 27	oveq12d 6319	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( g LMHom (ringLMod ` f ) ) = ( W LMHom (ringLMod ` F ) ) )
29	26, 28	eleq12d 2504	. . . . . . . . 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 6318	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h x ) = ( x ., x ) )
31	12	fveq2d 5881	. . . . . . . . . . . 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 2481	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` f ) = Z )
34	30, 33	eqeq12d 2444	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( x h x ) = ( 0g ` f ) <-> ( x ., x ) = Z ) )
35	15	fveq2d 5881	. . . . . . . . . . . 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 2481	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` g ) = .0. )
38	37	eqeq2d 2436	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x = ( 0g ` g ) <-> x = .0. ) )
39	34, 38	imbi12d 321	. . . . . . . . 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 5881	. . . . . . . . . . . . 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 2481	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( *r ` f ) = .* )
43	24	oveqd 6318	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h y ) = ( x ., y ) )
44	42, 43	fveq12d 5883	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( *r ` f ) ` ( x h y ) ) = ( .* ` ( x ., y ) ) )
45	44, 25	eqeq12d 2444	. . . . . . . . . 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 3039	. . . . . . . . 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 1335	. . . . . . . 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 3039	. . . . . . 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 715	. . . . . 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 3336	. . . . 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 3336	. . . 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 3336	. . 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 19177	. . 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 3231	. 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 986	. 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 255	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 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1868   A.wral 2775   _Vcvv 3081   [.wsbc 3299   |-> cmpt 4479   ` cfv 5597  (class class class)co 6301   Basecbs 15106   *rcstv 15177  Scalarcsca 15178   .icip 15180   0gc0g 15323   *Ringcsr 18057   LMHom clmhm 18227   LVecclvec 18310  ringLModcrglmod 18377   PreHilcphl 19175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-nul 4551

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-iota 5561  df-fv 5605  df-ov 6304  df-phl 19177

This theorem is referenced by:  phllvec  19180  phlsrng  19182  phllmhm  19183  ipcj  19185  ipeq0  19189  isphld  19205  phlpropd  19206