Definition df-shsum 9188

Description: Define subspace sum in S_ℋ. See shsumvalt 9192, shsumval2 9275, and shsumval3 9276 for its value.

Assertion

Ref	Expression
df-shsum	⊢ +ℋ = {⟨⟨x, y⟩, z⟩∣((x ∈ Sℋ ⋀ y ∈ Sℋ ) ⋀ z = {w ∈ ℋ ∣∃v ∈ x ∃u ∈ y w = (v +h u)})}

Distinct variable group:   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-shsum

Step	Hyp	Ref	Expression
1		cph 8739	. 2 class +ℋ
2		vx	. . . . . . 7 set x
3	2	cv 952	. . . . . 6 class x
4		csh 8736	. . . . . 6 class Sℋ
5	3, 4	wcel 955	. . . . 5 wff x ∈ Sℋ
6		vy	. . . . . . 7 set y
7	6	cv 952	. . . . . 6 class y
8	7, 4	wcel 955	. . . . 5 wff y ∈ Sℋ
9	5, 8	wa 223	. . . 4 wff (x ∈ Sℋ ⋀ y ∈ Sℋ )
10		vz	. . . . . 6 set z
11	10	cv 952	. . . . 5 class z
12		vw	. . . . . . . . . 10 set w
13	12	cv 952	. . . . . . . . 9 class w
14		vv	. . . . . . . . . . 11 set v
15	14	cv 952	. . . . . . . . . 10 class v
16		vu	. . . . . . . . . . 11 set u
17	16	cv 952	. . . . . . . . . 10 class u
18		cva 8728	. . . . . . . . . 10 class +h
19	15, 17, 18	co 3948	. . . . . . . . 9 class (v +h u)
20	13, 19	wceq 953	. . . . . . . 8 wff w = (v +h u)
21	20, 16, 7	wrex 1638	. . . . . . 7 wff ∃u ∈ y w = (v +h u)
22	21, 14, 3	wrex 1638	. . . . . 6 wff ∃v ∈ x ∃u ∈ y w = (v +h u)
23		chil 8727	. . . . . 6 class ℋ
24	22, 12, 23	crab 1640	. . . . 5 class {w ∈ ℋ ∣∃v ∈ x ∃u ∈ y w = (v +h u)}
25	11, 24	wceq 953	. . . 4 wff z = {w ∈ ℋ ∣∃v ∈ x ∃u ∈ y w = (v +h u)}
26	9, 25	wa 223	. . 3 wff ((x ∈ Sℋ ⋀ y ∈ Sℋ ) ⋀ z = {w ∈ ℋ ∣∃v ∈ x ∃u ∈ y w = (v +h u)})
27	26, 2, 6, 10	copab2 3949	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ Sℋ ⋀ y ∈ Sℋ ) ⋀ z = {w ∈ ℋ ∣∃v ∈ x ∃u ∈ y w = (v +h u)})}
28	1, 27	wceq 953	1 wff +ℋ = {⟨⟨x, y⟩, z⟩∣((x ∈ Sℋ ⋀ y ∈ Sℋ ) ⋀ z = {w ∈ ℋ ∣∃v ∈ x ∃u ∈ y w = (v +h u)})}

This definition is referenced by:  shsumvalt 9192

Copyright terms: Public domain