Theorem iscph 19086

Description: A complex pre-Hilbert space is a pre-Hilbert space over a quadratically closed subfield of the complexes, with a norm defined (Contributed by Mario Carneiro, 8-Oct-2015.)

Hypotheses

Ref	Expression
iscph.v	|- V = ( Base ` W )
iscph.h	|- ., = ( .i ` W )
iscph.n	|- N = ( norm ` W )
iscph.f	|- F = (Scalar ` W )
iscph.k	|- K = ( Base ` F )

Assertion

Ref	Expression
iscph	|- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) /\ ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) )

Distinct variable group:   x, W

Allowed substitution hints:   F( x)   ., ( x)   K( x)   N( x)   V( x)

Proof of Theorem iscph

Dummy variables f k w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3490	. . . . 5 |- ( W e. ( PreHil i^i NrmMod ) <-> ( W e. PreHil /\ W e. NrmMod ) )
2	1	anbi1i 677	. . . 4 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( ( W e. PreHil /\ W e. NrmMod ) /\ F = (ℂfld ↾s K ) ) )
3		df-3an 938	. . . 4 |- ( ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) <-> ( ( W e. PreHil /\ W e. NrmMod ) /\ F = (ℂfld ↾s K ) ) )
4	2, 3	bitr4i 244	. . 3 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) )
5	4	anbi1i 677	. 2 |- ( ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) )
6		fvex 5701	. . . . . 6 |- (Scalar ` w ) e. _V
7	6	a1i 11	. . . . 5 |- ( w = W -> (Scalar ` w ) e. _V )
8		fvex 5701	. . . . . . 7 |- ( Base ` f ) e. _V
9	8	a1i 11	. . . . . 6 |- ( ( w = W /\ f = (Scalar ` w ) ) -> ( Base ` f ) e. _V )
10		simplr 732	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = (Scalar ` w ) )
11		simpll 731	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> w = W )
12	11	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = (Scalar ` W ) )
13		iscph.f	. . . . . . . . . . 11 |- F = (Scalar ` W )
14	12, 13	syl6eqr 2454	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = F )
15	10, 14	eqtrd 2436	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = F )
16		simpr 448	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = ( Base ` f ) )
17	15	fveq2d 5691	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = ( Base ` F ) )
18		iscph.k	. . . . . . . . . . . 12 |- K = ( Base ` F )
19	17, 18	syl6eqr 2454	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = K )
20	16, 19	eqtrd 2436	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = K )
21	20	oveq2d 6056	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (ℂfld ↾s k ) = (ℂfld ↾s K ) )
22	15, 21	eqeq12d 2418	. . . . . . . 8 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( f = (ℂfld ↾s k ) <-> F = (ℂfld ↾s K ) ) )
23	20	ineq1d 3501	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( k i^i ( 0 [,) +oo ) ) = ( K i^i ( 0 [,) +oo ) ) )
24	23	imaeq2d 5162	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( sqr " ( k i^i ( 0 [,) +oo ) ) ) = ( sqr " ( K i^i ( 0 [,) +oo ) ) ) )
25	24, 20	sseq12d 3337	. . . . . . . 8 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k <-> ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K ) )
26	11	fveq2d 5691	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = ( norm ` W ) )
27		iscph.n	. . . . . . . . . 10 |- N = ( norm ` W )
28	26, 27	syl6eqr 2454	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = N )
29	11	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = ( Base ` W ) )
30		iscph.v	. . . . . . . . . . 11 |- V = ( Base ` W )
31	29, 30	syl6eqr 2454	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = V )
32	11	fveq2d 5691	. . . . . . . . . . . . 13 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ( .i ` W ) )
33		iscph.h	. . . . . . . . . . . . 13 |- ., = ( .i ` W )
34	32, 33	syl6eqr 2454	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ., )
35	34	oveqd 6057	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( x ( .i ` w ) x ) = ( x ., x ) )
36	35	fveq2d 5691	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( sqr ` ( x ( .i ` w ) x ) ) = ( sqr ` ( x ., x ) ) )
37	31, 36	mpteq12dv 4247	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) = ( x e. V |-> ( sqr ` ( x ., x ) ) ) )
38	28, 37	eqeq12d 2418	. . . . . . . 8 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) <-> N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) )
39	22, 25, 38	3anbi123d 1254	. . . . . . 7 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = (ℂfld ↾s K ) /\ ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) )
40		3anass 940	. . . . . . 7 |- ( ( F = (ℂfld ↾s K ) /\ ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) <-> ( F = (ℂfld ↾s K ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) )
41	39, 40	syl6bb 253	. . . . . 6 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = (ℂfld ↾s K ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) ) )
42	9, 41	sbcied 3157	. . . . 5 |- ( ( w = W /\ f = (Scalar ` w ) ) -> ( [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = (ℂfld ↾s K ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) ) )
43	7, 42	sbcied 3157	. . . 4 |- ( w = W -> ( [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = (ℂfld ↾s K ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) ) )
44		df-cph 19084	. . . 4 |- CPreHil = { w e. ( PreHil i^i NrmMod ) | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) }
45	43, 44	elrab2 3054	. . 3 |- ( W e. CPreHil <-> ( W e. ( PreHil i^i NrmMod ) /\ ( F = (ℂfld ↾s K ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) ) )
46		anass 631	. . 3 |- ( ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) <-> ( W e. ( PreHil i^i NrmMod ) /\ ( F = (ℂfld ↾s K ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) ) )
47	45, 46	bitr4i 244	. 2 |- ( W e. CPreHil <-> ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) )
48		3anass 940	. 2 |- ( ( ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) /\ ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) /\ ( ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) ) )
49	5, 47, 48	3bitr4i 269	1 |- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) /\ ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) )

Syntax hints:   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   _Vcvv 2916   [.wsbc 3121   i^i cin 3279   C_ wss 3280   e. cmpt 4226   "cima 4840   ` cfv 5413  (class class class)co 6040   0cc0 8946   +oocpnf 9073   [,)cico 10874   sqrcsqr 11993   Basecbs 13424   ↾_s cress 13425  Scalarcsca 13487   .icip 13489  ℂ_fldccnfld 16658   PreHilcphl 16810   normcnm 18577  NrmModcnlm 18581   CPreHilccph 19082

This theorem is referenced by:  cphphl  19087  cphnlm  19088  cphsca  19095  cphsqrcl  19100  cphnmfval  19108  tchcph  19147

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-xp 4843  df-cnv 4845  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fv 5421  df-ov 6043  df-cph 19084