Theorem hosmvalt 5487

Description: Value of sum of two Hilbert space operators.

Assertion

Ref	Expression
hosmvalt	|- ((S:H~-->H~ /\ T:H~-->H~) -> (S +P T) = {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))})

Distinct variable group(s):   x,y,S   x,T,y

Proof of Theorem hosmvalt

Step	Hyp	Ref	Expression
1		ax-hilex 4983	. . . 4 |- H~ e. V
2		oprex 3018	. . . . 5 |- ((S` x) +v (T` x)) e. V
3		cleqid 1102	. . . . 5 |- {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))} = {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))}
4	2, 3	fnopab2 2747	. . . 4 |- {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))} Fn H~
5		fnex 2740	. . . 4 |- (H~ e. V -> ({<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))} Fn H~ -> {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))} e. V))
6	1, 4, 5	mp2 43	. . 3 |- {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))} e. V
7		fveq1 2831	. . . . . . 7 |- (f = S -> (f` x) = (S` x))
8	7	opreq1d 3012	. . . . . 6 |- (f = S -> ((f` x) +v (g` x)) = ((S` x) +v (g` x)))
9	8	cleq2d 1112	. . . . 5 |- (f = S -> (y = ((f` x) +v (g` x)) <-> y = ((S` x) +v (g` x))))
10	9	anbi2d 468	. . . 4 |- (f = S -> ((x e. H~ /\ y = ((f` x) +v (g` x))) <-> (x e. H~ /\ y = ((S` x) +v (g` x)))))
11	10	biopabdv 2102	. . 3 |- (f = S -> {<.x, y>. | (x e. H~ /\ y = ((f` x) +v (g` x)))} = {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (g` x)))})
12		fveq1 2831	. . . . . . 7 |- (g = T -> (g` x) = (T` x))
13	12	opreq2d 3013	. . . . . 6 |- (g = T -> ((S` x) +v (g` x)) = ((S` x) +v (T` x)))
14	13	cleq2d 1112	. . . . 5 |- (g = T -> (y = ((S` x) +v (g` x)) <-> y = ((S` x) +v (T` x))))
15	14	anbi2d 468	. . . 4 |- (g = T -> ((x e. H~ /\ y = ((S` x) +v (g` x))) <-> (x e. H~ /\ y = ((S` x) +v (T` x)))))
16	15	biopabdv 2102	. . 3 |- (g = T -> {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (g` x)))} = {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))})
17		df-hosum 5485	. . . 4 |- +P = {<.<.f, g>., h>. | ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) +v (g` x)))})}
18		visset 1350	. . . . . . . 8 |- f e. V
19		feq1 2748	. . . . . . . 8 |- (x = f -> (x:H~-->H~ <-> f:H~-->H~))
20	18, 19	elab 1415	. . . . . . 7 |- (f e. {x | x:H~-->H~} <-> f:H~-->H~)
21		visset 1350	. . . . . . . 8 |- g e. V
22		feq1 2748	. . . . . . . 8 |- (x = g -> (x:H~-->H~ <-> g:H~-->H~))
23	21, 22	elab 1415	. . . . . . 7 |- (g e. {x | x:H~-->H~} <-> g:H~-->H~)
24	20, 23	anbi12i 369	. . . . . 6 |- ((f e. {x | x:H~-->H~} /\ g e. {x | x:H~-->H~}) <-> (f:H~-->H~ /\ g:H~-->H~))
25	24	anbi1i 368	. . . . 5 |- (((f e. {x | x:H~-->H~} /\ g e. {x | x:H~-->H~}) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) +v (g` x)))}) <-> ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) +v (g` x)))}))
26	25	bioprabi 3027	. . . 4 |- {<.<.f, g>., h>. | ((f e. {x | x:H~-->H~} /\ g e. {x | x:H~-->H~}) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) +v (g` x)))})} = {<.<.f, g>., h>. | ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) +v (g` x)))})}
27	17, 26	eqtr4 1122	. . 3 |- +P = {<.<.f, g>., h>. | ((f e. {x | x:H~-->H~} /\ g e. {x | x:H~-->H~}) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) +v (g` x)))})}
28	6, 11, 16, 27	oprabval2 3051	. 2 |- ((S e. {x | x:H~-->H~} /\ T e. {x | x:H~-->H~}) -> (S +P T) = {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))})
29		fex 2771	. . . 4 |- (H~ e. V -> (S:H~-->H~ -> S e. V))
30	1, 29	ax-mp 6	. . 3 |- (S:H~-->H~ -> S e. V)
31		feq1 2748	. . 3 |- (x = S -> (x:H~-->H~ <-> S:H~-->H~))
32	30, 31	elab3g 1420	. 2 |- (S e. {x | x:H~-->H~} <-> S:H~-->H~)
33		fex 2771	. . . 4 |- (H~ e. V -> (T:H~-->H~ -> T e. V))
34	1, 33	ax-mp 6	. . 3 |- (T:H~-->H~ -> T e. V)
35		feq1 2748	. . 3 |- (x = T -> (x:H~-->H~ <-> T:H~-->H~))
36	34, 35	elab3g 1420	. 2 |- (T e. {x | x:H~-->H~} <-> T:H~-->H~)
37	28, 32, 36	syl2anbr 351	1 |- ((S:H~-->H~ /\ T:H~-->H~) -> (S +P T) = {<.x, y>. | (x e. H~ /\ y = ((S` x) +v (T` x)))})

Syntax hints:   -> wi 2   /\ wa 196  {cab 1090   = wceq 1091   e. wcel 1092  Vcvv 1348  {copab 2055   Fn wfn 2417  -->wf 2418  ` cfv 2422  (class class class)co 3001  {copab2 3002  H~chil 4958   +v cva 4959   +P chos 4977

This theorem is referenced by:  hosvalt 5489  hosf 5602

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-hilex 4983

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-fv 2438  df-opr 3003  df-oprab 3004  df-hosum 5485

metamath.org