Theorem rrxcph 22429

Description: Generalized Euclidean real spaces are pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)

Hypotheses

Ref	Expression
rrxval.r	|- H = (ℝ^ ` I )
rrxbase.b	|- B = ( Base ` H )

Assertion

Ref	Expression
rrxcph	|- ( I e. V -> H e. CPreHil )

Proof of Theorem rrxcph

Dummy variables f x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rrxval.r	. . 3 |- H = (ℝ^ ` I )
2	1	rrxval 22424	. 2 |- ( I e. V -> H = (toCHil ` (RRfld freeLMod I ) ) )
3		eqid 2471	. . 3 |- (toCHil ` (RRfld freeLMod I ) ) = (toCHil ` (RRfld freeLMod I ) )
4		eqid 2471	. . 3 |- ( Base ` (RRfld freeLMod I ) ) = ( Base ` (RRfld freeLMod I ) )
5		eqid 2471	. . 3 |- (Scalar ` (RRfld freeLMod I ) ) = (Scalar ` (RRfld freeLMod I ) )
6		eqid 2471	. . . 4 |- (RRfld freeLMod I ) = (RRfld freeLMod I )
7		rebase 19251	. . . 4 |- RR = ( Base ` RRfld )
8		remulr 19256	. . . 4 |- x. = ( .r ` RRfld )
9		eqid 2471	. . . 4 |- ( .i ` (RRfld freeLMod I ) ) = ( .i ` (RRfld freeLMod I ) )
10		eqid 2471	. . . 4 |- ( 0g ` (RRfld freeLMod I ) ) = ( 0g ` (RRfld freeLMod I ) )
11		re0g 19257	. . . 4 |- 0 = ( 0g ` RRfld )
12		refldcj 19265	. . . 4 |- * = ( *r ` RRfld )
13		refld 19264	. . . . 5 |- RRfld e. Field
14	13	a1i 11	. . . 4 |- ( I e. V -> RRfld e. Field )
15		fconstmpt 4883	. . . . 5 |- ( I X. { 0 } ) = ( x e. I |-> 0 )
16	6, 7, 4	frlmbasf 19400	. . . . . . . 8 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> f : I --> RR )
17		ffn 5739	. . . . . . . 8 |- ( f : I --> RR -> f Fn I )
18	16, 17	syl 17	. . . . . . 7 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> f Fn I )
19	18	3adant3 1050	. . . . . 6 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> f Fn I )
20		simpl 464	. . . . . . . . . . . . . . . . 17 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> I e. V )
21	13	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> RRfld e. Field )
22		simpr 468	. . . . . . . . . . . . . . . . 17 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> f e. ( Base ` (RRfld freeLMod I ) ) )
23	6, 7, 8, 4, 9	frlmipval 19414	. . . . . . . . . . . . . . . . 17 |- ( ( ( I e. V /\ RRfld e. Field ) /\ ( f e. ( Base ` (RRfld freeLMod I ) ) /\ f e. ( Base ` (RRfld freeLMod I ) ) ) ) -> ( f ( .i ` (RRfld freeLMod I ) ) f ) = (RRfld gsumg ( f oF x. f ) ) )
24	20, 21, 22, 22, 23	syl22anc 1293	. . . . . . . . . . . . . . . 16 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f ( .i ` (RRfld freeLMod I ) ) f ) = (RRfld gsumg ( f oF x. f ) ) )
25		ovex 6336	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f ` x ) x. ( f ` x ) ) e. _V
26	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. I ) -> ( ( f ` x ) x. ( f ` x ) ) e. _V )
27		inidm 3632	. . . . . . . . . . . . . . . . . . . 20 |- ( I i^i I ) = I
28		eqidd 2472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. I ) -> ( f ` x ) = ( f ` x ) )
29	18, 18, 20, 20, 27, 28, 28	offval 6557	. . . . . . . . . . . . . . . . . . 19 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f oF x. f ) = ( x e. I |-> ( ( f ` x ) x. ( f ` x ) ) ) )
30	18, 18, 20, 20, 27, 28, 28	ofval 6559	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. I ) -> ( ( f oF x. f ) ` x ) = ( ( f ` x ) x. ( f ` x ) ) )
31	16	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. I ) -> ( f ` x ) e. RR )
32	31, 31	remulcld 9689	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. I ) -> ( ( f ` x ) x. ( f ` x ) ) e. RR )
33	30, 32	eqeltrd 2549	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. I ) -> ( ( f oF x. f ) ` x ) e. RR )
34	26, 29, 33	fmpt2d 6069	. . . . . . . . . . . . . . . . . 18 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f oF x. f ) : I --> RR )
35		ovex 6336	. . . . . . . . . . . . . . . . . . . 20 |- ( f oF x. f ) e. _V
36	35	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f oF x. f ) e. _V )
37		ffun 5742	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f oF x. f ) : I --> RR -> Fun ( f oF x. f ) )
38	34, 37	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> Fun ( f oF x. f ) )
39	6, 11, 4	frlmbasfsupp 19398	. . . . . . . . . . . . . . . . . . 19 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> f finSupp 0 )
40		0red 9662	. . . . . . . . . . . . . . . . . . . 20 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> 0 e. RR )
41		simpr 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. RR ) -> x e. RR )
42	41	recnd 9687	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. RR ) -> x e. CC )
43	42	mul02d 9849	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. RR ) -> ( 0 x. x ) = 0 )
44	20, 40, 16, 16, 43	suppofss1d 6971	. . . . . . . . . . . . . . . . . . 19 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( ( f oF x. f ) supp 0 ) C_ ( f supp 0 ) )
45		fsuppsssupp 7917	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( f oF x. f ) e. _V /\ Fun ( f oF x. f ) ) /\ ( f finSupp 0 /\ ( ( f oF x. f ) supp 0 ) C_ ( f supp 0 ) ) ) -> ( f oF x. f ) finSupp 0 )
46	36, 38, 39, 44, 45	syl22anc 1293	. . . . . . . . . . . . . . . . . 18 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f oF x. f ) finSupp 0 )
47		regsumsupp 19267	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f oF x. f ) : I --> RR /\ ( f oF x. f ) finSupp 0 /\ I e. V ) -> (RRfld gsumg ( f oF x. f ) ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f oF x. f ) ` x ) )
48	34, 46, 20, 47	syl3anc 1292	. . . . . . . . . . . . . . . . 17 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> (RRfld gsumg ( f oF x. f ) ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f oF x. f ) ` x ) )
49		suppssdm 6946	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f supp 0 ) C_ dom f
50		fdm 5745	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f : I --> RR -> dom f = I )
51	16, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> dom f = I )
52	49, 51	syl5sseq 3466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f supp 0 ) C_ I )
53	44, 52	sstrd 3428	. . . . . . . . . . . . . . . . . . . 20 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( ( f oF x. f ) supp 0 ) C_ I )
54	53	sselda 3418	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> x e. I )
55	54, 30	syldan 478	. . . . . . . . . . . . . . . . . 18 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f oF x. f ) ` x ) = ( ( f ` x ) x. ( f ` x ) ) )
56	55	sumeq2dv 13846	. . . . . . . . . . . . . . . . 17 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f oF x. f ) ` x ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
57	48, 56	eqtrd 2505	. . . . . . . . . . . . . . . 16 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> (RRfld gsumg ( f oF x. f ) ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
58	24, 57	eqtrd 2505	. . . . . . . . . . . . . . 15 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f ( .i ` (RRfld freeLMod I ) ) f ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
59	58	3adant3 1050	. . . . . . . . . . . . . 14 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> ( f ( .i ` (RRfld freeLMod I ) ) f ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
60		simp3 1032	. . . . . . . . . . . . . 14 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 )
61	59, 60	eqtr3d 2507	. . . . . . . . . . . . 13 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 )
62	39	fsuppimpd 7908	. . . . . . . . . . . . . . . 16 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( f supp 0 ) e. Fin )
63		ssfi 7810	. . . . . . . . . . . . . . . 16 |- ( ( ( f supp 0 ) e. Fin /\ ( ( f oF x. f ) supp 0 ) C_ ( f supp 0 ) ) -> ( ( f oF x. f ) supp 0 ) e. Fin )
64	62, 44, 63	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( ( f oF x. f ) supp 0 ) e. Fin )
65	54, 32	syldan 478	. . . . . . . . . . . . . . 15 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) x. ( f ` x ) ) e. RR )
66	31	msqge0d 10203	. . . . . . . . . . . . . . . 16 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. I ) -> 0 <_ ( ( f ` x ) x. ( f ` x ) ) )
67	54, 66	syldan 478	. . . . . . . . . . . . . . 15 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> 0 <_ ( ( f ` x ) x. ( f ` x ) ) )
68	64, 65, 67	fsum00 13935	. . . . . . . . . . . . . 14 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 <-> A. x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 ) )
69	68	3adant3 1050	. . . . . . . . . . . . 13 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> ( sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 <-> A. x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 ) )
70	61, 69	mpbid 215	. . . . . . . . . . . 12 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> A. x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 )
71	70	r19.21bi 2776	. . . . . . . . . . 11 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) x. ( f ` x ) ) = 0 )
72	71	adantlr 729	. . . . . . . . . 10 |- ( ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) x. ( f ` x ) ) = 0 )
73	31	3adantl3 1188	. . . . . . . . . . . . 13 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f ` x ) e. RR )
74	73	recnd 9687	. . . . . . . . . . . 12 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f ` x ) e. CC )
75	74, 74	mul0ord 10284	. . . . . . . . . . 11 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f ` x ) x. ( f ` x ) ) = 0 <-> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) ) )
76	75	adantr 472	. . . . . . . . . 10 |- ( ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( ( f ` x ) x. ( f ` x ) ) = 0 <-> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) ) )
77	72, 76	mpbid 215	. . . . . . . . 9 |- ( ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) )
78		oridm 523	. . . . . . . . 9 |- ( ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) <-> ( f ` x ) = 0 )
79	77, 78	sylib 201	. . . . . . . 8 |- ( ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( f ` x ) = 0 )
80	34	3adant3 1050	. . . . . . . . . . 11 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> ( f oF x. f ) : I --> RR )
81	80	adantr 472	. . . . . . . . . 10 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f oF x. f ) : I --> RR )
82		ssid 3437	. . . . . . . . . . 11 |- ( ( f oF x. f ) supp 0 ) C_ ( ( f oF x. f ) supp 0 )
83	82	a1i 11	. . . . . . . . . 10 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( f oF x. f ) supp 0 ) C_ ( ( f oF x. f ) supp 0 ) )
84		simpl1 1033	. . . . . . . . . 10 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> I e. V )
85		0red 9662	. . . . . . . . . 10 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> 0 e. RR )
86	81, 83, 84, 85	suppssr 6965	. . . . . . . . 9 |- ( ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) -> ( ( f oF x. f ) ` x ) = 0 )
87	30	3adantl3 1188	. . . . . . . . . . . . 13 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( f oF x. f ) ` x ) = ( ( f ` x ) x. ( f ` x ) ) )
88	87	eqeq1d 2473	. . . . . . . . . . . 12 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f oF x. f ) ` x ) = 0 <-> ( ( f ` x ) x. ( f ` x ) ) = 0 ) )
89	88, 75	bitrd 261	. . . . . . . . . . 11 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f oF x. f ) ` x ) = 0 <-> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) ) )
90	89, 78	syl6bb 269	. . . . . . . . . 10 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f oF x. f ) ` x ) = 0 <-> ( f ` x ) = 0 ) )
91	90	biimpa 492	. . . . . . . . 9 |- ( ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ ( ( f oF x. f ) ` x ) = 0 ) -> ( f ` x ) = 0 )
92	86, 91	syldan 478	. . . . . . . 8 |- ( ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) -> ( f ` x ) = 0 )
93		undif 3839	. . . . . . . . . . . . 13 |- ( ( ( f oF x. f ) supp 0 ) C_ I <-> ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) = I )
94	53, 93	sylib 201	. . . . . . . . . . . 12 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) = I )
95	94	eleq2d 2534	. . . . . . . . . . 11 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> ( x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) <-> x e. I ) )
96	95	3adant3 1050	. . . . . . . . . 10 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> ( x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) <-> x e. I ) )
97	96	biimpar 493	. . . . . . . . 9 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) )
98		elun 3565	. . . . . . . . 9 |- ( x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) <-> ( x e. ( ( f oF x. f ) supp 0 ) \/ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) )
99	97, 98	sylib 201	. . . . . . . 8 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( x e. ( ( f oF x. f ) supp 0 ) \/ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) )
100	79, 92, 99	mpjaodan 803	. . . . . . 7 |- ( ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f ` x ) = 0 )
101	100	ralrimiva 2809	. . . . . 6 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> A. x e. I ( f ` x ) = 0 )
102		fconstfv 6143	. . . . . . 7 |- ( f : I --> { 0 } <-> ( f Fn I /\ A. x e. I ( f ` x ) = 0 ) )
103		c0ex 9655	. . . . . . . 8 |- 0 e. _V
104	103	fconst2 6137	. . . . . . 7 |- ( f : I --> { 0 } <-> f = ( I X. { 0 } ) )
105	102, 104	sylbb1 220	. . . . . 6 |- ( ( f Fn I /\ A. x e. I ( f ` x ) = 0 ) -> f = ( I X. { 0 } ) )
106	19, 101, 105	syl2anc 673	. . . . 5 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> f = ( I X. { 0 } ) )
107		isfld 18062	. . . . . . . . . . 11 |- (RRfld e. Field <-> (RRfld e. DivRing /\ RRfld e. CRing ) )
108	13, 107	mpbi 213	. . . . . . . . . 10 |- (RRfld e. DivRing /\ RRfld e. CRing )
109	108	simpli 465	. . . . . . . . 9 |- RRfld e. DivRing
110		drngring 18060	. . . . . . . . 9 |- (RRfld e. DivRing -> RRfld e. Ring )
111	109, 110	ax-mp 5	. . . . . . . 8 |- RRfld e. Ring
112	6, 11	frlm0 19394	. . . . . . . 8 |- ( (RRfld e. Ring /\ I e. V ) -> ( I X. { 0 } ) = ( 0g ` (RRfld freeLMod I ) ) )
113	111, 112	mpan 684	. . . . . . 7 |- ( I e. V -> ( I X. { 0 } ) = ( 0g ` (RRfld freeLMod I ) ) )
114	15, 113	syl5reqr 2520	. . . . . 6 |- ( I e. V -> ( 0g ` (RRfld freeLMod I ) ) = ( x e. I |-> 0 ) )
115	114	3ad2ant1 1051	. . . . 5 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> ( 0g ` (RRfld freeLMod I ) ) = ( x e. I |-> 0 ) )
116	15, 106, 115	3eqtr4a 2531	. . . 4 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) /\ ( f ( .i ` (RRfld freeLMod I ) ) f ) = 0 ) -> f = ( 0g ` (RRfld freeLMod I ) ) )
117		cjre 13279	. . . . 5 |- ( x e. RR -> ( * ` x ) = x )
118	117	adantl 473	. . . 4 |- ( ( I e. V /\ x e. RR ) -> ( * ` x ) = x )
119		id 22	. . . 4 |- ( I e. V -> I e. V )
120	6, 7, 8, 4, 9, 10, 11, 12, 14, 116, 118, 119	frlmphl 19416	. . 3 |- ( I e. V -> (RRfld freeLMod I ) e. PreHil )
121		df-refld 19250	. . . 4 |- RRfld = (ℂfld ↾s RR )
122	6	frlmsca 19393	. . . . 5 |- ( (RRfld e. Field /\ I e. V ) -> RRfld = (Scalar ` (RRfld freeLMod I ) ) )
123	13, 122	mpan 684	. . . 4 |- ( I e. V -> RRfld = (Scalar ` (RRfld freeLMod I ) ) )
124	121, 123	syl5reqr 2520	. . 3 |- ( I e. V -> (Scalar ` (RRfld freeLMod I ) ) = (ℂfld ↾s RR ) )
125		simpr1 1036	. . . 4 |- ( ( I e. V /\ ( f e. RR /\ f e. RR /\ 0 <_ f ) ) -> f e. RR )
126		simpr3 1038	. . . 4 |- ( ( I e. V /\ ( f e. RR /\ f e. RR /\ 0 <_ f ) ) -> 0 <_ f )
127	125, 126	resqrtcld 13556	. . 3 |- ( ( I e. V /\ ( f e. RR /\ f e. RR /\ 0 <_ f ) ) -> ( sqr ` f ) e. RR )
128	64, 65, 67	fsumge0 13932	. . . . 5 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> 0 <_ sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
129	128, 57	breqtrrd 4422	. . . 4 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> 0 <_ (RRfld gsumg ( f oF x. f ) ) )
130	129, 24	breqtrrd 4422	. . 3 |- ( ( I e. V /\ f e. ( Base ` (RRfld freeLMod I ) ) ) -> 0 <_ ( f ( .i ` (RRfld freeLMod I ) ) f ) )
131	3, 4, 5, 120, 124, 9, 127, 130	tchcph 22289	. 2 |- ( I e. V -> (toCHil ` (RRfld freeLMod I ) ) e. CPreHil )
132	2, 131	eqeltrd 2549	1 |- ( I e. V -> H e. CPreHil )

Syntax hints:   -> wi 4   <-> wb 189   \/ wo 375   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   A.wral 2756   _Vcvv 3031   \ cdif 3387   u. cun 3388   C_ wss 3390   {csn 3959   class class class wbr 4395   |-> cmpt 4454   X. cxp 4837   dom cdm 4839   Fun wfun 5583   Fn wfn 5584   -->wf 5585   ` cfv 5589  (class class class)co 6308   oFcof 6548   supp csupp 6933   Fincfn 7587   finSupp cfsupp 7901   RRcr 9556   0cc0 9557   x. cmul 9562   <_ cle 9694   *ccj 13236   sum_csu 13829   Basecbs 15199   ↾_s cress 15200  Scalarcsca 15271   .icip 15273   0gc0g 15416   gsum_g cgsu 15417   Ringcrg 17858   CRingccrg 17859   DivRingcdr 18053  Fieldcfield 18054  ℂ_fldccnfld 19047  RRfldcrefld 19249   freeLMod cfrlm 19386   CPreHilccph 22222  toCHilctch 22223  ℝ^crrx 22420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-tpos 6991  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ico 11666  df-fz 11811  df-fzo 11943  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-prds 15424  df-pws 15426  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-mhm 16660  df-submnd 16661  df-grp 16751  df-minusg 16752  df-sbg 16753  df-subg 16892  df-ghm 16959  df-cntz 17049  df-cmn 17510  df-abl 17511  df-mgp 17802  df-ur 17814  df-ring 17860  df-cring 17861  df-oppr 17929  df-dvdsr 17947  df-unit 17948  df-invr 17978  df-dvr 17989  df-rnghom 18021  df-drng 18055  df-field 18056  df-subrg 18084  df-abv 18123  df-staf 18151  df-srng 18152  df-lmod 18171  df-lss 18234  df-lmhm 18323  df-lvec 18404  df-sra 18473  df-rgmod 18474  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-cnfld 19048  df-refld 19250  df-phl 19270  df-dsmm 19372  df-frlm 19387  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-xms 21413  df-ms 21414  df-nm 21675  df-ngp 21676  df-tng 21677  df-nrg 21678  df-nlm 21679  df-clm 22172  df-cph 22224  df-tch 22225  df-rrx 22422

This theorem is referenced by:  rrxngp  38263