Theorem isphl 18530

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 5862	. . . . 5 |- ( Base ` g ) e. _V
2	1	a1i 11	. . . 4 |- ( g = W -> ( Base ` g ) e. _V )
3		fvex 5862	. . . . . 6 |- ( .i ` g ) e. _V
4	3	a1i 11	. . . . 5 |- ( ( g = W /\ v = ( Base ` g ) ) -> ( .i ` g ) e. _V )
5		fvex 5862	. . . . . . 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 5856	. . . . . . . . . 10 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = (Scalar ` W ) )
10		isphl.f	. . . . . . . . . 10 |- F = (Scalar ` W )
11	9, 10	syl6eqr 2500	. . . . . . . . 9 |- ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> (Scalar ` g ) = F )
12	7, 11	sylan9eqr 2504	. . . . . . . 8 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> f = F )
13	12	eleq1d 2510	. . . . . . 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 5856	. . . . . . . . . 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 2500	. . . . . . . . 9 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( Base ` g ) = V )
19	14, 18	eqtrd 2482	. . . . . . . 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 5856	. . . . . . . . . . . . . 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 2500	. . . . . . . . . . . . 13 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( .i ` g ) = ., )
24	20, 23	eqtrd 2482	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> h = ., )
25	24	oveqd 6294	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( y h x ) = ( y ., x ) )
26	19, 25	mpteq12dv 4511	. . . . . . . . . 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 5856	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> (ringLMod ` f ) = (ringLMod ` F ) )
28	15, 27	oveq12d 6295	. . . . . . . . . 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 6294	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h x ) = ( x ., x ) )
31	12	fveq2d 5856	. . . . . . . . . . . 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 2500	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` f ) = Z )
34	30, 33	eqeq12d 2463	. . . . . . . . . 10 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( x h x ) = ( 0g ` f ) <-> ( x ., x ) = Z ) )
35	15	fveq2d 5856	. . . . . . . . . . . 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 2500	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( 0g ` g ) = .0. )
38	37	eqeq2d 2455	. . . . . . . . . 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 5856	. . . . . . . . . . . . 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 2500	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( *r ` f ) = .* )
43	24	oveqd 6294	. . . . . . . . . . . 12 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( x h y ) = ( x ., y ) )
44	42, 43	fveq12d 5858	. . . . . . . . . . 11 |- ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = (Scalar ` g ) ) -> ( ( *r ` f ) ` ( x h y ) ) = ( .* ` ( x ., y ) ) )
45	44, 25	eqeq12d 2463	. . . . . . . . . 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 3052	. . . . . . . . 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 1298	. . . . . . . 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 3052	. . . . . . 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 3348	. . . . 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 3348	. . . 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 3348	. . 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 18528	. . 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 3243	. 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 976	. 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 972   = wceq 1381   e. wcel 1802   A.wral 2791   _Vcvv 3093   [.wsbc 3311   |-> cmpt 4491   ` cfv 5574  (class class class)co 6277   Basecbs 14504   *rcstv 14571  Scalarcsca 14572   .icip 14574   0gc0g 14709   *Ringcsr 17361   LMHom clmhm 17533   LVecclvec 17616  ringLModcrglmod 17683   PreHilcphl 18526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-nul 4562

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-iota 5537  df-fv 5582  df-ov 6280  df-phl 18528

This theorem is referenced by:  phllvec  18531  phlsrng  18533  phllmhm  18534  ipcj  18536  ipeq0  18540  isphld  18556  phlpropd  18557