Definition df-pjdif 5486

Description: Define the difference of two Hilbert space operators. Definition of [Beran] p. 111.

Assertion

Ref	Expression
df-pjdif	|- -P = {<.<.f, g>., h>. | ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) -v (g` x)))})}

Distinct variable group(s):   f,g,h,x,y

Detailed syntax breakdown of Definition df-pjdif

Step	Hyp	Ref	Expression
1		cpjd 4978	. 2 class -P
2		chil 4958	. . . . . 6 class H~
3		vf	. . . . . . 7 set f
4	3	cv 1089	. . . . . 6 class f
5	2, 2, 4	wf 2418	. . . . 5 wff f:H~-->H~
6		vg	. . . . . . 7 set g
7	6	cv 1089	. . . . . 6 class g
8	2, 2, 7	wf 2418	. . . . 5 wff g:H~-->H~
9	5, 8	wa 196	. . . 4 wff (f:H~-->H~ /\ g:H~-->H~)
10		vh	. . . . . 6 set h
11	10	cv 1089	. . . . 5 class h
12		vx	. . . . . . . . 9 set x
13	12	cv 1089	. . . . . . . 8 class x
14	13, 2	wcel 1092	. . . . . . 7 wff x e. H~
15		vy	. . . . . . . . 9 set y
16	15	cv 1089	. . . . . . . 8 class y
17	13, 4	cfv 2422	. . . . . . . . 9 class (f` x)
18	13, 7	cfv 2422	. . . . . . . . 9 class (g` x)
19		cmv 4962	. . . . . . . . 9 class -v
20	17, 18, 19	co 3001	. . . . . . . 8 class ((f` x) -v (g` x))
21	16, 20	wceq 1091	. . . . . . 7 wff y = ((f` x) -v (g` x))
22	14, 21	wa 196	. . . . . 6 wff (x e. H~ /\ y = ((f` x) -v (g` x)))
23	22, 12, 15	copab 2055	. . . . 5 class {<.x, y>. | (x e. H~ /\ y = ((f` x) -v (g` x)))}
24	11, 23	wceq 1091	. . . 4 wff h = {<.x, y>. | (x e. H~ /\ y = ((f` x) -v (g` x)))}
25	9, 24	wa 196	. . 3 wff ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) -v (g` x)))})
26	25, 3, 6, 10	copab2 3002	. 2 class {<.<.f, g>., h>. | ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) -v (g` x)))})}
27	1, 26	wceq 1091	1 wff -P = {<.<.f, g>., h>. | ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) -v (g` x)))})}

This definition is referenced by:  hodmvalt 5488

metamath.org