Theorem iscph 22090

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 3592	. . . . 5 |- ( W e. ( PreHil i^i NrmMod ) <-> ( W e. PreHil /\ W e. NrmMod ) )
2	1	anbi1i 699	. . . 4 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( ( W e. PreHil /\ W e. NrmMod ) /\ F = (ℂfld ↾s K ) ) )
3		df-3an 984	. . . 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 255	. . 3 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) )
5	4	anbi1i 699	. 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 5835	. . . . . 6 |- (Scalar ` w ) e. _V
7	6	a1i 11	. . . . 5 |- ( w = W -> (Scalar ` w ) e. _V )
8		fvex 5835	. . . . . . 7 |- ( Base ` f ) e. _V
9	8	a1i 11	. . . . . 6 |- ( ( w = W /\ f = (Scalar ` w ) ) -> ( Base ` f ) e. _V )
10		simplr 760	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = (Scalar ` w ) )
11		simpll 758	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> w = W )
12	11	fveq2d 5829	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = (Scalar ` W ) )
13		iscph.f	. . . . . . . . . . 11 |- F = (Scalar ` W )
14	12, 13	syl6eqr 2480	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = F )
15	10, 14	eqtrd 2462	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = F )
16		simpr 462	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = ( Base ` f ) )
17	15	fveq2d 5829	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = ( Base ` F ) )
18		iscph.k	. . . . . . . . . . . 12 |- K = ( Base ` F )
19	17, 18	syl6eqr 2480	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = K )
20	16, 19	eqtrd 2462	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = K )
21	20	oveq2d 6265	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (ℂfld ↾s k ) = (ℂfld ↾s K ) )
22	15, 21	eqeq12d 2443	. . . . . . . 8 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( f = (ℂfld ↾s k ) <-> F = (ℂfld ↾s K ) ) )
23	20	ineq1d 3606	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( k i^i ( 0 [,) +oo ) ) = ( K i^i ( 0 [,) +oo ) ) )
24	23	imaeq2d 5130	. . . . . . . . 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 3436	. . . . . . . 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 5829	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = ( norm ` W ) )
27		iscph.n	. . . . . . . . . 10 |- N = ( norm ` W )
28	26, 27	syl6eqr 2480	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = N )
29	11	fveq2d 5829	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = ( Base ` W ) )
30		iscph.v	. . . . . . . . . . 11 |- V = ( Base ` W )
31	29, 30	syl6eqr 2480	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = V )
32	11	fveq2d 5829	. . . . . . . . . . . . 13 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ( .i ` W ) )
33		iscph.h	. . . . . . . . . . . . 13 |- ., = ( .i ` W )
34	32, 33	syl6eqr 2480	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ., )
35	34	oveqd 6266	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( x ( .i ` w ) x ) = ( x ., x ) )
36	35	fveq2d 5829	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( sqr ` ( x ( .i ` w ) x ) ) = ( sqr ` ( x ., x ) ) )
37	31, 36	mpteq12dv 4445	. . . . . . . . 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 2443	. . . . . . . 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 1335	. . . . . . 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 986	. . . . . . 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 264	. . . . . 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 3279	. . . . 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 3279	. . . 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 22088	. . . 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 3173	. . 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 653	. . 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 255	. 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 986	. 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 280	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 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1872   _Vcvv 3022   [.wsbc 3242   i^i cin 3378   C_ wss 3379   |-> cmpt 4425   "cima 4799   ` cfv 5544  (class class class)co 6249   0cc0 9490   +oocpnf 9623   [,)cico 11588   sqrcsqrt 13240   Basecbs 15064   ↾_s cress 15065  Scalarcsca 15136   .icip 15138  ℂ_fldccnfld 18913   PreHilcphl 19133   normcnm 21533  NrmModcnlm 21537   CPreHilccph 22086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-nul 4498

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-xp 4802  df-cnv 4804  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fv 5552  df-ov 6252  df-cph 22088

This theorem is referenced by:  cphphl  22091  cphnlm  22092  cphsca  22099  cphsqrtcl  22104  cphnmfval  22112  tchcph  22153