Theorem iscph 21483

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 3669	. . . . 5 |- ( W e. ( PreHil i^i NrmMod ) <-> ( W e. PreHil /\ W e. NrmMod ) )
2	1	anbi1i 695	. . . 4 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( ( W e. PreHil /\ W e. NrmMod ) /\ F = (ℂfld ↾s K ) ) )
3		df-3an 974	. . . 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 252	. . 3 |- ( ( W e. ( PreHil i^i NrmMod ) /\ F = (ℂfld ↾s K ) ) <-> ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) )
5	4	anbi1i 695	. 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 5862	. . . . . 6 |- (Scalar ` w ) e. _V
7	6	a1i 11	. . . . 5 |- ( w = W -> (Scalar ` w ) e. _V )
8		fvex 5862	. . . . . . 7 |- ( Base ` f ) e. _V
9	8	a1i 11	. . . . . 6 |- ( ( w = W /\ f = (Scalar ` w ) ) -> ( Base ` f ) e. _V )
10		simplr 754	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = (Scalar ` w ) )
11		simpll 753	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> w = W )
12	11	fveq2d 5856	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = (Scalar ` W ) )
13		iscph.f	. . . . . . . . . . 11 |- F = (Scalar ` W )
14	12, 13	syl6eqr 2500	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (Scalar ` w ) = F )
15	10, 14	eqtrd 2482	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = F )
16		simpr 461	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = ( Base ` f ) )
17	15	fveq2d 5856	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = ( Base ` F ) )
18		iscph.k	. . . . . . . . . . . 12 |- K = ( Base ` F )
19	17, 18	syl6eqr 2500	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = K )
20	16, 19	eqtrd 2482	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = K )
21	20	oveq2d 6293	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> (ℂfld ↾s k ) = (ℂfld ↾s K ) )
22	15, 21	eqeq12d 2463	. . . . . . . 8 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( f = (ℂfld ↾s k ) <-> F = (ℂfld ↾s K ) ) )
23	20	ineq1d 3681	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( k i^i ( 0 [,) +oo ) ) = ( K i^i ( 0 [,) +oo ) ) )
24	23	imaeq2d 5323	. . . . . . . . 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 3515	. . . . . . . 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 5856	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = ( norm ` W ) )
27		iscph.n	. . . . . . . . . 10 |- N = ( norm ` W )
28	26, 27	syl6eqr 2500	. . . . . . . . 9 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = N )
29	11	fveq2d 5856	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = ( Base ` W ) )
30		iscph.v	. . . . . . . . . . 11 |- V = ( Base ` W )
31	29, 30	syl6eqr 2500	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = V )
32	11	fveq2d 5856	. . . . . . . . . . . . 13 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ( .i ` W ) )
33		iscph.h	. . . . . . . . . . . . 13 |- ., = ( .i ` W )
34	32, 33	syl6eqr 2500	. . . . . . . . . . . 12 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ., )
35	34	oveqd 6294	. . . . . . . . . . 11 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( x ( .i ` w ) x ) = ( x ., x ) )
36	35	fveq2d 5856	. . . . . . . . . 10 |- ( ( ( w = W /\ f = (Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( sqr ` ( x ( .i ` w ) x ) ) = ( sqr ` ( x ., x ) ) )
37	31, 36	mpteq12dv 4511	. . . . . . . . 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 2463	. . . . . . . 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 1298	. . . . . . 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 976	. . . . . . 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 261	. . . . . 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 3348	. . . . 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 3348	. . . 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 21481	. . . 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 3243	. . 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 649	. . 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 252	. 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 976	. 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 277	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 184   /\ wa 369   /\ w3a 972   = wceq 1381   e. wcel 1802   _Vcvv 3093   [.wsbc 3311   i^i cin 3457   C_ wss 3458   |-> cmpt 4491   "cima 4988   ` cfv 5574  (class class class)co 6277   0cc0 9490   +oocpnf 9623   [,)cico 11535   sqrcsqrt 13040   Basecbs 14504   ↾_s cress 14505  Scalarcsca 14572   .icip 14574  ℂ_fldccnfld 18288   PreHilcphl 18526   normcnm 20963  NrmModcnlm 20967   CPreHilccph 21479

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-xp 4991  df-cnv 4993  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fv 5582  df-ov 6280  df-cph 21481

This theorem is referenced by:  cphphl  21484  cphnlm  21485  cphsca  21492  cphsqrtcl  21497  cphnmfval  21505  tchcph  21546