Theorem shscl 9281

Description: Closure of subspace sum.

Hypotheses

Ref	Expression
shscl.1	|- A e. SH
shscl.2	|- B e. SH

Assertion

Ref	Expression
shscl	|- (A +H B) e. SH

Proof of Theorem shscl

Step	Hyp	Ref	Expression
1		sh 9078	. 2 |- ((A +H B) e. SH <-> (((A +H B) (_ H~ /\ 0h e. (A +H B)) /\ (A.x e. (A +H B)A.y e. (A +H B)(x +h y) e. (A +H B) /\ A.x e. CC A.y e. (A +H B)(x .h y) e. (A +H B))))
2		shscl.1	. . . . 5 |- A e. SH
3		shscl.2	. . . . 5 |- B e. SH
4		shsumvalt 9277	. . . . 5 |- ((A e. SH /\ B e. SH) -> (A +H B) = {z e. H~ | E.x e. A E.y e. B z = (x +h y)})
5	2, 3, 4	mp2an 697	. . . 4 |- (A +H B) = {z e. H~ | E.x e. A E.y e. B z = (x +h y)}
6		ssrab2 2131	. . . 4 |- {z e. H~ | E.x e. A E.y e. B z = (x +h y)} (_ H~
7	5, 6	eqsstr 2091	. . 3 |- (A +H B) (_ H~
8		sh0 9084	. . . . . 6 |- (A e. SH -> 0h e. A)
9	2, 8	ax-mp 7	. . . . 5 |- 0h e. A
10		sh0 9084	. . . . . 6 |- (B e. SH -> 0h e. B)
11	3, 10	ax-mp 7	. . . . 5 |- 0h e. B
12		ax-hv0cl 8873	. . . . . . 7 |- 0h e. H~
13	12	hvaddid2 8898	. . . . . 6 |- (0h +h 0h) = 0h
14	13	eqcomi 1479	. . . . 5 |- 0h = (0h +h 0h)
15		rcla4eopr 3990	. . . . 5 |- ((0h e. A /\ 0h e. B /\ 0h = (0h +h 0h)) -> E.x e. A E.y e. B 0h = (x +h y))
16	9, 11, 14, 15	mp3an 916	. . . 4 |- E.x e. A E.y e. B 0h = (x +h y)
17	2, 3	shsel 9280	. . . 4 |- (0h e. (A +H B) <-> E.x e. A E.y e. B 0h = (x +h y))
18	16, 17	mpbir 190	. . 3 |- 0h e. (A +H B)
19	7, 18	pm3.2i 285	. 2 |- ((A +H B) (_ H~ /\ 0h e. (A +H B))
20		rcla4eopr 3990	. . . . . . . . . . . 12 |- (((z +h v) e. A /\ (w +h u) e. B /\ (x +h y) = ((z +h v) +h (w +h u))) -> E.f e. A E.g e. B (x +h y) = (f +h g))
21		shaddcltOLD 9086	. . . . . . . . . . . . . . 15 |- (A e. SH -> ((z e. A /\ v e. A) -> (z +h v) e. A))
22	2, 21	ax-mp 7	. . . . . . . . . . . . . 14 |- ((z e. A /\ v e. A) -> (z +h v) e. A)
23	22	ad2ant2r 409	. . . . . . . . . . . . 13 |- (((z e. A /\ w e. B) /\ (v e. A /\ u e. B)) -> (z +h v) e. A)
24	23	ad2ant2r 409	. . . . . . . . . . . 12 |- ((((z e. A /\ w e. B) /\ x = (z +h w)) /\ ((v e. A /\ u e. B) /\ y = (v +h u))) -> (z +h v) e. A)
25		shaddcltOLD 9086	. . . . . . . . . . . . . . 15 |- (B e. SH -> ((w e. B /\ u e. B) -> (w +h u) e. B))
26	3, 25	ax-mp 7	. . . . . . . . . . . . . 14 |- ((w e. B /\ u e. B) -> (w +h u) e. B)
27	26	ad2ant2l 408	. . . . . . . . . . . . 13 |- (((z e. A /\ w e. B) /\ (v e. A /\ u e. B)) -> (w +h u) e. B)
28	27	ad2ant2r 409	. . . . . . . . . . . 12 |- ((((z e. A /\ w e. B) /\ x = (z +h w)) /\ ((v e. A /\ u e. B) /\ y = (v +h u))) -> (w +h u) e. B)
29		opreq12 3970	. . . . . . . . . . . . . 14 |- ((x = (z +h w) /\ y = (v +h u)) -> (x +h y) = ((z +h w) +h (v +h u)))
30	29	ad2ant2l 408	. . . . . . . . . . . . 13 |- ((((z e. A /\ w e. B) /\ x = (z +h w)) /\ ((v e. A /\ u e. B) /\ y = (v +h u))) -> (x +h y) = ((z +h w) +h (v +h u)))
31		hvadd4t 8905	. . . . . . . . . . . . . . . 16 |- (((z e. H~ /\ v e. H~) /\ (w e. H~ /\ u e. H~)) -> ((z +h v) +h (w +h u)) = ((z +h w) +h (v +h u)))
32	2	shel 9082	. . . . . . . . . . . . . . . . 17 |- (z e. A -> z e. H~)
33	2	shel 9082	. . . . . . . . . . . . . . . . 17 |- (v e. A -> v e. H~)
34	32, 33	anim12i 333	. . . . . . . . . . . . . . . 16 |- ((z e. A /\ v e. A) -> (z e. H~ /\ v e. H~))
35	3	shel 9082	. . . . . . . . . . . . . . . . 17 |- (w e. B -> w e. H~)
36	3	shel 9082	. . . . . . . . . . . . . . . . 17 |- (u e. B -> u e. H~)
37	35, 36	anim12i 333	. . . . . . . . . . . . . . . 16 |- ((w e. B /\ u e. B) -> (w e. H~ /\ u e. H~))
38	31, 34, 37	syl2an 454	. . . . . . . . . . . . . . 15 |- (((z e. A /\ v e. A) /\ (w e. B /\ u e. B)) -> ((z +h v) +h (w +h u)) = ((z +h w) +h (v +h u)))
39	38	an4s 508	. . . . . . . . . . . . . 14 |- (((z e. A /\ w e. B) /\ (v e. A /\ u e. B)) -> ((z +h v) +h (w +h u)) = ((z +h w) +h (v +h u)))
40	39	ad2ant2r 409	. . . . . . . . . . . . 13 |- ((((z e. A /\ w e. B) /\ x = (z +h w)) /\ ((v e. A /\ u e. B) /\ y = (v +h u))) -> ((z +h v) +h (w +h u)) = ((z +h w) +h (v +h u)))
41	30, 40	eqtr4d 1510	. . . . . . . . . . . 12 |- ((((z e. A /\ w e. B) /\ x = (z +h w)) /\ ((v e. A /\ u e. B) /\ y = (v +h u))) -> (x +h y) = ((z +h v) +h (w +h u)))
42	20, 24, 28, 41	syl3anc 858	. . . . . . . . . . 11 |- ((((z e. A /\ w e. B) /\ x = (z +h w)) /\ ((v e. A /\ u e. B) /\ y = (v +h u))) -> E.f e. A E.g e. B (x +h y) = (f +h g))
43	42	ancoms 436	. . . . . . . . . 10 |- ((((v e. A /\ u e. B) /\ y = (v +h u)) /\ ((z e. A /\ w e. B) /\ x = (z +h w))) -> E.f e. A E.g e. B (x +h y) = (f +h g))
44	43	exp43 384	. . . . . . . . 9 |- ((v e. A /\ u e. B) -> (y = (v +h u) -> ((z e. A /\ w e. B) -> (x = (z +h w) -> E.f e. A E.g e. B (x +h y) = (f +h g)))))
45	44	r19.23aivv 1748	. . . . . . . 8 |- (E.v e. A E.u e. B y = (v +h u) -> ((z e. A /\ w e. B) -> (x = (z +h w) -> E.f e. A E.g e. B (x +h y) = (f +h g))))
46	45	com3l 34	. . . . . . 7 |- ((z e. A /\ w e. B) -> (x = (z +h w) -> (E.v e. A E.u e. B y = (v +h u) -> E.f e. A E.g e. B (x +h y) = (f +h g))))
47	46	r19.23aivv 1748	. . . . . 6 |- (E.z e. A E.w e. B x = (z +h w) -> (E.v e. A E.u e. B y = (v +h u) -> E.f e. A E.g e. B (x +h y) = (f +h g)))
48	47	imp 350	. . . . 5 |- ((E.z e. A E.w e. B x = (z +h w) /\ E.v e. A E.u e. B y = (v +h u)) -> E.f e. A E.g e. B (x +h y) = (f +h g))
49	2, 3	shsel 9280	. . . . . 6 |- (x e. (A +H B) <-> E.z e. A E.w e. B x = (z +h w))
50	2, 3	shsel 9280	. . . . . 6 |- (y e. (A +H B) <-> E.v e. A E.u e. B y = (v +h u))
51	49, 50	anbi12i 482	. . . . 5 |- ((x e. (A +H B) /\ y e. (A +H B)) <-> (E.z e. A E.w e. B x = (z +h w) /\ E.v e. A E.u e. B y = (v +h u)))
52	2, 3	shsel 9280	. . . . 5 |- ((x +h y) e. (A +H B) <-> E.f e. A E.g e. B (x +h y) = (f +h g))
53	48, 51, 52	3imtr4 219	. . . 4 |- ((x e. (A +H B) /\ y e. (A +H B)) -> (x +h y) e. (A +H B))
54	53	rgen2a 1699	. . 3 |- A.x e. (A +H B)A.y e. (A +H B)(x +h y) e. (A +H B)
55		rcla4eopr 3990	. . . . . . . . . . 11 |- (((x .h v) e. A /\ (x .h u) e. B /\ (x .h y) = ((x .h v) +h (x .h u))) -> E.f e. A E.g e. B (x .h y) = (f +h g))
56		shmulclt 9087	. . . . . . . . . . . . 13 |- ((A e. SH /\ x e. CC /\ v e. A) -> (x .h v) e. A)
57	2, 56	mp3an1 903	. . . . . . . . . . . 12 |- ((x e. CC /\ v e. A) -> (x .h v) e. A)
58	57	adantrr 395	. . . . . . . . . . 11 |- ((x e. CC /\ (v e. A /\ (u e. B /\ y = (v +h u)))) -> (x .h v) e. A)
59		shmulclt 9087	. . . . . . . . . . . . . 14 |- ((B e. SH /\ x e. CC /\ u e. B) -> (x .h u) e. B)
60	3, 59	mp3an1 903	. . . . . . . . . . . . 13 |- ((x e. CC /\ u e. B) -> (x .h u) e. B)
61	60	adantrr 395	. . . . . . . . . . . 12 |- ((x e. CC /\ (u e. B /\ y = (v +h u))) -> (x .h u) e. B)
62	61	adantrl 394	. . . . . . . . . . 11 |- ((x e. CC /\