Theorem shscl 5282

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		shscl.1	. . . . . 6 |- A e. SH
2		shscl.2	. . . . . 6 |- B e. SH
3		shsumvalt 5279	. . . . . 6 |- ((A e. SH /\ B e. SH) -> (A +H B) = {z e. H~ | E.x e. A E.y e. B z = (x +v y)})
4	1, 2, 3	mp2an 520	. . . . 5 |- (A +H B) = {z e. H~ | E.x e. A E.y e. B z = (x +v y)}
5		ssrab 1556	. . . . 5 |- {z e. H~ | E.x e. A E.y e. B z = (x +v y)} (_ H~
6	4, 5	eqsstr 1530	. . . 4 |- (A +H B) (_ H~
7		sh0 5122	. . . . . . . 8 |- (A e. SH -> 0v e. A)
8	1, 7	ax-mp 6	. . . . . . 7 |- 0v e. A
9		sh0 5122	. . . . . . . 8 |- (B e. SH -> 0v e. B)
10	2, 9	ax-mp 6	. . . . . . 7 |- 0v e. B
11	8, 10	pm3.2i 234	. . . . . 6 |- (0v e. A /\ 0v e. B)
12		ax-hvzercl 4987	. . . . . . . 8 |- 0v e. H~
13	12	hvaddid2 5008	. . . . . . 7 |- (0v +v 0v) = 0v
14	13	cleqcomi 1105	. . . . . 6 |- 0v = (0v +v 0v)
15		opreq1 3006	. . . . . . . 8 |- (x = 0v -> (x +v y) = (0v +v y))
16	15	cleq2d 1112	. . . . . . 7 |- (x = 0v -> (0v = (x +v y) <-> 0v = (0v +v y)))
17		opreq2 3007	. . . . . . . 8 |- (y = 0v -> (0v +v y) = (0v +v 0v))
18	17	cleq2d 1112	. . . . . . 7 |- (y = 0v -> (0v = (0v +v y) <-> 0v = (0v +v 0v)))
19	16, 18	rcla42ev 1405	. . . . . 6 |- (((0v e. A /\ 0v e. B) /\ 0v = (0v +v 0v)) -> E.x e. A E.y e. B 0v = (x +v y))
20	11, 14, 19	mp2an 520	. . . . 5 |- E.x e. A E.y e. B 0v = (x +v y)
21	1, 2	shsel 5281	. . . . 5 |- (0v e. (A +H B) <-> E.x e. A E.y e. B 0v = (x +v y))
22	20, 21	mpbir 165	. . . 4 |- 0v e. (A +H B)
23	6, 22	pm3.2i 234	. . 3 |- ((A +H B) (_ H~ /\ 0v e. (A +H B))
24		opreq1 3006	. . . . . . . . . . . . . . . . . . . 20 |- (f = (z +v v) -> (f +v g) = ((z +v v) +v g))
25	24	cleq2d 1112	. . . . . . . . . . . . . . . . . . 19 |- (f = (z +v v) -> ((x +v y) = (f +v g) <-> (x +v y) = ((z +v v) +v g)))
26		opreq2 3007	. . . . . . . . . . . . . . . . . . . 20 |- (g = (w +v u) -> ((z +v v) +v g) = ((z +v v) +v (w +v u)))
27	26	cleq2d 1112	. . . . . . . . . . . . . . . . . . 19 |- (g = (w +v u) -> ((x +v y) = ((z +v v) +v g) <-> (x +v y) = ((z +v v) +v (w +v u))))
28	25, 27	rcla42ev 1405	. . . . . . . . . . . . . . . . . 18 |- ((((z +v v) e. A /\ (w +v u) e. B) /\ (x +v y) = ((z +v v) +v (w +v u))) -> E.f e. A E.g e. B (x +v y) = (f +v g))
29		shaddclt 5123	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. SH -> ((z e. A /\ v e. A) -> (z +v v) e. A))
30	1, 29	ax-mp 6	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. A /\ v e. A) -> (z +v v) e. A)
31		shaddclt 5123	. . . . . . . . . . . . . . . . . . . . 21 |- (B e. SH -> ((w e. B /\ u e. B) -> (w +v u) e. B))
32	2, 31	ax-mp 6	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. B /\ u e. B) -> (w +v u) e. B)
33	30, 32	anim12i 268	. . . . . . . . . . . . . . . . . . 19 |- (((z e. A /\ v e. A) /\ (w e. B /\ u e. B)) -> ((z +v v) e. A /\ (w +v u) e. B))
34	33	adantrr 312	. . . . . . . . . . . . . . . . . 18 |- (((z e. A /\ v e. A) /\ ((w e. B /\ u e. B) /\ (x = (z +v w) /\ y = (v +v u)))) -> ((z +v v) e. A /\ (w +v u) e. B))
35		opreq12 3008	. . . . . . . . . . . . . . . . . . . 20 |- ((x = (z +v w) /\ y = (v +v u)) -> (x +v y) = ((z +v w) +v (v +v u)))
36		hvadd4t 5013	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. H~ /\ v e. H~) /\ (w e. H~ /\ u e. H~)) -> ((z +v v) +v (w +v u)) = ((z +v w) +v (v +v u)))
37	1	shel 5120	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. A -> z e. H~)
38	1	shel 5120	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. A -> v e. H~)
39	37, 38	anim12i 268	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. A /\ v e. A) -> (z e. H~ /\ v e. H~))
40	2	shel 5120	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w e. B -> w e. H~)
41	2	shel 5120	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. B -> u e. H~)
42	40, 41	anim12i 268	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w e. B /\ u e. B) -> (w e. H~ /\ u e. H~))
43	36, 39, 42	syl2an 349	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. A /\ v e. A) /\ (w e. B /\ u e. B)) -> ((z +v v) +v (w +v u)) = ((z +v w) +v (v +v u)))
44	43	cleqcomd 1106	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. A /\ v e. A) /\ (w e. B /\ u e. B)) -> ((z +v w) +v (v +v u)) = ((z +v v) +v (w +v u)))
45	35, 44	sylan9eqr 1145	. . . . . . . . . . . . . . . . . . 19 |- ((((z e. A /\ v e. A) /\ (w e. B /\ u e. B)) /\ (x = (z +v w) /\ y = (v +v u))) -> (x +v y) = ((z +v v) +v (w +v u)))
46	45	anasss 337	. . . . . . . . . . . . . . . . . 18 |- (((z e. A /\ v e. A) /\ ((w e. B /\ u e. B) /\ (x = (z +v w) /\ y = (v +v u)))) -> (x +v y) = ((z +v v) +v (w +v u)))
47	28, 34, 46	sylanc 361	. . . . . . . . . . . . . . . . 17 |- (((z e. A /\ v e. A) /\ ((w e. B /\ u e. B) /\ (x = (z +v w) /\ y = (v +v u)))) -> E.f e. A E.g e. B (x +v y) = (f +v g))
48		an4 388	. . . . . . . . . . . . . . . . 17 |- (((w e. B /\ x = (z +v w)) /\ (u e. B /\ y = (v +v u))) <-> ((w e. B /\ u e. B) /\ (x = (z +v w) /\ y = (v +v u))))
49	47, 48	sylan2b 347	. . . . . . . . . . . . . . . 16 |- (((z e. A /\ v e. A) /\ ((w e. B /\ x = (z +v w)) /\ (u e. B /\ y = (v +v u)))) -> E.f e. A E.g e. B (x +v y) = (f +v g))
50	49	an4s 390	. . . . . . . . . . . . . . 15 |- (((z e. A /\ (w e. B /\ x = (z +v w))) /\ (v e. A /\ (u e. B /\ y = (v +v u)))) -> E.f e. A E.g e. B (x +v y) = (f +v g))
51	50	exp42 300	. . . . . . . . . . . . . 14 |- (z e. A -> (w e. B -> (x = (z +v w) -> ((v e. A /\ (u e. B /\ y = (v +v u))) -> E.f e. A E.g e. B (x +v y) = (f +v g)))))
52	51	imp 277	. . . . . . . . . . . . 13 |- ((z e. A /\ w e. B) -> (x = (z +v w) -> ((v e. A /\ (u e. B /\ y = (v +v u))) -> E.f e. A E.g e. B (x +v y) = (f +v g))))
53	52	com3r 35	. . . . . . . . . . . 12 |- ((v e. A /\ (u e. B /\ y = (v +v u))) -> ((z e. A /\ w e. B) -> (x = (z +v w) -> E.f e. A E.g e. B (x +v y) = (f +v g))))
54	53	exp32 294	. . . . . . . . . . 11 |- (v e. A -> (u e. B -> (y = (v +v u) -> ((z e. A /\ w e. B) -> (x = (z +v w) -> E.f e. A E.g e. B (x +v y) = (f +v g))))))
55	54	imp 277	. . . . . . . . . 10 |- ((v e. A /\ u e. B) -> (y = (v +v u) -> ((z e. A /\ w e. B) -> (x = (z +v w) -> E.f e. A E.g e. B (x +v y) = (f +v g)))))
56	55	r19.23aivv 1287	. . . . . . . . 9 |- (E.v e. A E.u e. B y = (v +v u) -> ((z e. A /\ w e. B) -> (x = (z +v w) -> E.f e. A E.g e. B (x +v y) = (f +v g))))
57	56	com3l 34	. . . . . . . 8 |- ((z e. A /\ w e. B) -> (x = (z +v w) -> (E.v e. A E.u e. B y = (v +v u) -> E.f e. A E.g e. B (x +v y) = (f +v g))))
58	57	r19.23aivv 1287	. . . . . . 7 |- (E.z e. A E.w e. B x = (z +v w) -> (E.v e. A E.u e. B y = (v +v u) -> E.f e. A E.g e. B (x +v y) = (f +v g)))
59	58	imp 277	. . . . . 6 |- ((E.z e. A E.w e. B x = (z +v w) /\ E.v e. A E.u e. B y = (v +v u)) -> E.f e. A E.g e. B (x +v y) = (f +v g))
60	1, 2	shsel 5281	. . . . . . 7 |- (x e. (A +H B) <-> E.z e. A E.w e. B x = (z +v w))
61	1, 2	shsel 5281	. . . . . . 7 |- (y e. (A +H B) <-> E.v e. A E.u e. B y = (v +v u))
62	60, 61	anbi12i 369	. . . . . 6 |- ((x e. (A +H B) /\ y e. (A +H B)) <-> (E.z e. A