Theorem spanunsn 5482

Description: The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton.

Hypotheses

Ref	Expression
spanunsn.1	|- A e. CH
spanunsn.2	|- B e. H~

Assertion

Ref	Expression
spanunsn	|- (span` (A u. {B})) = (span` (A u. {((Proj` (_|_` A))` B)}))

Proof of Theorem spanunsn

Step	Hyp	Ref	Expression
1		spanunsn.1	. . . . . . 7 |- A e. CH
2	1	chshi 5132	. . . . . 6 |- A e. SH
3		spanunsn.2	. . . . . . . 8 |- B e. H~
4		snssi 1851	. . . . . . . 8 |- (B e. H~ -> {B} (_ H~)
5	3, 4	ax-mp 6	. . . . . . 7 |- {B} (_ H~
6		spanclt 5305	. . . . . . 7 |- ({B} (_ H~ -> (span` {B}) e. SH)
7	5, 6	ax-mp 6	. . . . . 6 |- (span` {B}) e. SH
8	2, 7	shsel 5281	. . . . 5 |- (x e. (A +H (span` {B})) <-> E.y e. A E.z e. (span` {B})x = (y +v z))
9		eleq1 1149	. . . . . . . . . . . 12 |- (x = (y +v (w .s B)) -> (x e. (A +H (span` {((Proj` (_|_` A))` B)})) <-> (y +v (w .s B)) e. (A +H (span` {((Proj` (_|_` A))` B)}))))
10	9	biimparc 327	. . . . . . . . . . 11 |- (((y +v (w .s B)) e. (A +H (span` {((Proj` (_|_` A))` B)})) /\ x = (y +v (w .s B))) -> x e. (A +H (span` {((Proj` (_|_` A))` B)})))
11		opreq1 3006	. . . . . . . . . . . . . . 15 |- (v = (y +v (w .s ((Proj` A)` B))) -> (v +v u) = ((y +v (w .s ((Proj` A)` B))) +v u))
12	11	cleq2d 1112	. . . . . . . . . . . . . 14 |- (v = (y +v (w .s ((Proj` A)` B))) -> ((y +v (w .s B)) = (v +v u) <-> (y +v (w .s B)) = ((y +v (w .s ((Proj` A)` B))) +v u)))
13		opreq2 3007	. . . . . . . . . . . . . . 15 |- (u = (w .s ((Proj` (_|_` A))` B)) -> ((y +v (w .s ((Proj` A)` B))) +v u) = ((y +v (w .s ((Proj` A)` B))) +v (w .s ((Proj` (_|_` A))` B))))
14	13	cleq2d 1112	. . . . . . . . . . . . . 14 |- (u = (w .s ((Proj` (_|_` A))` B)) -> ((y +v (w .s B)) = ((y +v (w .s ((Proj` A)` B))) +v u) <-> (y +v (w .s B)) = ((y +v (w .s ((Proj` A)` B))) +v (w .s ((Proj` (_|_` A))` B)))))
15	12, 14	rcla42ev 1405	. . . . . . . . . . . . 13 |- ((((y +v (w .s ((Proj` A)` B))) e. A /\ (w .s ((Proj` (_|_` A))` B)) e. (span` {((Proj` (_|_` A))` B)})) /\ (y +v (w .s B)) = ((y +v (w .s ((Proj` A)` B))) +v (w .s ((Proj` (_|_` A))` B)))) -> E.v e. A E.u e. (span` {((Proj` (_|_` A))` B)})(y +v (w .s B)) = (v +v u))
16		shaddclt 5123	. . . . . . . . . . . . . . . 16 |- (A e. SH -> ((y e. A /\ (w .s ((Proj` A)` B)) e. A) -> (y +v (w .s ((Proj` A)` B))) e. A))
17	1, 3	pjcli 5257	. . . . . . . . . . . . . . . . 17 |- ((Proj` A)` B) e. A
18		shmulclt 5124	. . . . . . . . . . . . . . . . . 18 |- (A e. SH -> ((w e. CC /\ ((Proj` A)` B) e. A) -> (w .s ((Proj` A)` B)) e. A))
19	2, 18	ax-mp 6	. . . . . . . . . . . . . . . . 17 |- ((w e. CC /\ ((Proj` A)` B) e. A) -> (w .s ((Proj` A)` B)) e. A)
20	17, 19	mpan2 519	. . . . . . . . . . . . . . . 16 |- (w e. CC -> (w .s ((Proj` A)` B)) e. A)
21	16, 20	sylan2i 357	. . . . . . . . . . . . . . 15 |- (A e. SH -> ((y e. A /\ w e. CC) -> (y +v (w .s ((Proj` A)` B))) e. A))
22	2, 21	ax-mp 6	. . . . . . . . . . . . . 14 |- ((y e. A /\ w e. CC) -> (y +v (w .s ((Proj` A)` B))) e. A)
23	1	chocl 5192	. . . . . . . . . . . . . . . . 17 |- (_|_` A) e. CH
24	23, 3	pjhcli 5258	. . . . . . . . . . . . . . . 16 |- ((Proj` (_|_` A))` B) e. H~
25		spansnmul 5469	. . . . . . . . . . . . . . . 16 |- ((((Proj` (_|_` A))` B) e. H~ /\ w e. CC) -> (w .s ((Proj` (_|_` A))` B)) e. (span` {((Proj` (_|_` A))` B)}))
26	24, 25	mpan 518	. . . . . . . . . . . . . . 15 |- (w e. CC -> (w .s ((Proj` (_|_` A))` B)) e. (span` {((Proj` (_|_` A))` B)}))
27	26	adantl 305	. . . . . . . . . . . . . 14 |- ((y e. A /\ w e. CC) -> (w .s ((Proj` (_|_` A))` B)) e. (span` {((Proj` (_|_` A))` B)}))
28	22, 27	jca 236	. . . . . . . . . . . . 13 |- ((y e. A /\ w e. CC) -> ((y +v (w .s ((Proj` A)` B))) e. A /\ (w .s ((Proj` (_|_` A))` B)) e. (span` {((Proj` (_|_` A))` B)})))
29	1, 3	pjhcli 5258	. . . . . . . . . . . . . . . . . 18 |- ((Proj` A)` B) e. H~
30		ax-hvdistr1 4993	. . . . . . . . . . . . . . . . . . 19 |- ((w e. CC /\ ((Proj` A)` B) e. H~ /\ ((Proj` (_|_` A))` B) e. H~) -> (w .s (((Proj` A)` B) +v ((Proj` (_|_` A))` B))) = ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B))))
31	24, 30	mp3an3 641	. . . . . . . . . . . . . . . . . 18 |- ((w e. CC /\ ((Proj` A)` B) e. H~) -> (w .s (((Proj` A)` B) +v ((Proj` (_|_` A))` B))) = ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B))))
32	29, 31	mpan2 519	. . . . . . . . . . . . . . . . 17 |- (w e. CC -> (w .s (((Proj` A)` B) +v ((Proj` (_|_` A))` B))) = ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B))))
33	1, 3	pjpj 5261	. . . . . . . . . . . . . . . . . 18 |- B = (((Proj` A)` B) +v ((Proj` (_|_` A))` B))
34	33	opreq2i 3010	. . . . . . . . . . . . . . . . 17 |- (w .s B) = (w .s (((Proj` A)` B) +v ((Proj` (_|_` A))` B)))
35	32, 34	syl5eq 1136	. . . . . . . . . . . . . . . 16 |- (w e. CC -> (w .s B) = ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B))))
36	35	adantl 305	. . . . . . . . . . . . . . 15 |- ((y e. A /\ w e. CC) -> (w .s B) = ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B))))
37	36	opreq2d 3013	. . . . . . . . . . . . . 14 |- ((y e. A /\ w e. CC) -> (y +v (w .s B)) = (y +v ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B)))))
38		ax-hvass 4986	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ (w .s ((Proj` A)` B)) e. H~ /\ (w .s ((Proj` (_|_` A))` B)) e. H~) -> ((y +v (w .s ((Proj` A)` B))) +v (w .s ((Proj` (_|_` A))` B))) = (y +v ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B)))))
39	38	3expb 613	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ ((w .s ((Proj` A)` B)) e. H~ /\ (w .s ((Proj` (_|_` A))` B)) e. H~)) -> ((y +v (w .s ((Proj` A)` B))) +v (w .s ((Proj` (_|_` A))` B))) = (y +v ((w .s ((Proj` A)` B)) +v (w .s ((Proj` (_|_` A))` B)))))
40	1	chel 5137	. . . . . . . . . . . . . . 15 |- (y e. A -> y e. H~)
41		ax-hvmulcl 4989	. . . . . . . . . . . . . . . . 17 |- ((w e. CC /\ ((Proj` A)` B) e. H~) -> (w .s ((Proj` A)` B)) e. H~)
42	29, 41	mpan2 519	. . . . . . . . . . . . . . . 16 |- (w e. CC -> (w .s ((Proj` A)` B)) e. H~)
43		ax-hvmulcl 4989	. . . . . . . . . . . . . . . . 17 |- ((w e. CC /\ ((Proj` (_|_` A))` B) e. H~) -> (w .s ((Proj` (_|_` A))` B)) e. H~)
44	24, 43	mpan2 519	. . . . . . . . . . . . . . . 16 |- (w e. CC -> (w .s ((Proj` (_|_` A))` B)) e. H~)
45	42, 44	jca 236	. . . . . . . . . . . . . . 15 |- (w e. CC