Theorem iscph 22196

Description: A complex pre-Hilbert space is a pre-Hilbert space over a quadratically closed subfield of the complex numbers, 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 3628	. . . . 5 |- ( W e. ( PreHil i^i NrmMod ) <-> ( W e. PreHil /\ W e. NrmMod ) )
2	1	anbi1i 706	. . . 4 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( ( W e. PreHil /\ W e. NrmMod ) /\ F = (ℂfld ↾s K ) ) )
3		df-3an 993	. . . 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 260	. . 3 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) )
5	4	anbi1i 706	. 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 5897	. . . . . 6 |- (Scalar ` w ) e. _V
7	6	a1i 11	. . . . 5 |- ( w = W -> (Scalar ` w ) e. _V )
8		fvex 5897	. . . . . . 7 |- ( Base ` f ) e. _V
9	8	a1i 11	. . . . . 6 |- ( ( w = W /\ f = (Scalar ` w ) ) -> ( Base ` f ) e. _V )
10		simplr 767	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = (Scalar ` w ) )
11		simpll 765	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> w = W )
12	11	fveq2d 5891	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = (Scalar ` W ) )
13		iscph.f	. . . . . . . . . . 11 |- F = (Scalar ` W )
14	12, 13	syl6eqr 2513	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = F )
15	10, 14	eqtrd 2495	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = F )
16		simpr 467	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = ( Base ` f ) )
17	15	fveq2d 5891	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = ( Base ` F ) )
18		iscph.k	. . . . . . . . . . . 12 |- K = ( Base ` F )
19	17, 18	syl6eqr 2513	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = K )
20	16, 19	eqtrd 2495	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = K )
21	20	oveq2d 6330	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (ℂfld ↾s k ) = (ℂfld ↾s K ) )
22	15, 21	eqeq12d 2476	. . . . . . . 8 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( f = (ℂfld ↾s k ) <-> F = (ℂfld ↾s K ) ) )
23	20	ineq1d 3644	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( k i^i ( 0 [,) +oo ) ) = ( K i^i ( 0 [,) +oo ) ) )
24	23	imaeq2d 5186	. . . . . . . . 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 3472	. . . . . . . 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 5891	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = ( norm ` W ) )
27		iscph.n	. . . . . . . . . 10 |- N = ( norm ` W )
28	26, 27	syl6eqr 2513	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = N )
29	11	fveq2d 5891	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = ( Base ` W ) )
30		iscph.v	. . . . . . . . . . 11 |- V = ( Base ` W )
31	29, 30	syl6eqr 2513	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = V )
32	11	fveq2d 5891	. . . . . . . . . . . . 13 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ( .i ` W ) )
33		iscph.h	. . . . . . . . . . . . 13 |- ., = ( .i ` W )
34	32, 33	syl6eqr 2513	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ., )
35	34	oveqd 6331	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( x ( .i ` w ) x ) = ( x ., x ) )
36	35	fveq2d 5891	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( sqr ` ( x ( .i ` w ) x ) ) = ( sqr ` ( x ., x ) ) )
37	31, 36	mpteq12dv 4494	. . . . . . . . 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 2476	. . . . . . . 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 1348	. . . . . . 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 995	. . . . . . 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 269	. . . . . 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 3315	. . . . 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 3315	. . . 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 22194	. . . 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 3209	. . 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 659	. . 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 260	. 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 995	. 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 285	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 189   /\ wa 375   /\ w3a 991   = wceq 1454   e. wcel 1897   _Vcvv 3056   [.wsbc 3278   i^i cin 3414   C_ wss 3415   |-> cmpt 4474   "cima 4855   ` cfv 5600  (class class class)co 6314   0cc0 9564   +oocpnf 9697   [,)cico 11665   sqrcsqrt 13344   Basecbs 15169   ↾_s cress 15170  Scalarcsca 15241   .icip 15243  ℂ_fldccnfld 19018   PreHilcphl 19239   normcnm 21639  NrmModcnlm 21643   CPreHilccph 22192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-nul 4547

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-xp 4858  df-cnv 4860  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fv 5608  df-ov 6317  df-cph 22194

This theorem is referenced by:  cphphl  22197  cphnlm  22198  cphsca  22205  cphsqrtcl  22210  cphnmfval  22218  tchcph  22259