Theorem spanunsn 9419

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 9018	. . . . . 6 |- A e. SH
3		spanunsn.2	. . . . . . . 8 |- B e. H~
4		snssi 2457	. . . . . . . 8 |- (B e. H~ -> {B} (_ H~)
5	3, 4	ax-mp 7	. . . . . . 7 |- {B} (_ H~
6		spanclt 9219	. . . . . . 7 |- ({B} (_ H~ -> (span` {B}) e. SH)
7	5, 6	ax-mp 7	. . . . . 6 |- (span` {B}) e. SH
8	2, 7	shsel 9195	. . . . 5 |- (x e. (A +H (span` {B})) <-> E.y e. A E.z e. (span` {B})x = (y +h z))
9		eleq1 1526	. . . . . . . . . . . 12 |- (x = (y +h (w .h B)) -> (x e. (A +H (span` {((proj` (_|_` A))` B)})) <-> (y +h (w .h B)) e. (A +H (span` {((proj` (_|_` A))` B)}))))
10	9	biimparc 419	. . . . . . . . . . 11 |- (((y +h (w .h B)) e. (A +H (span` {((proj` (_|_` A))` B)})) /\ x = (y +h (w .h B))) -> x e. (A +H (span` {((proj` (_|_` A))` B)})))
11		rcla4eopr 3975	. . . . . . . . . . . . 13 |- (((y +h (w .h ((proj` A)` B))) e. A /\ (w .h ((proj` (_|_` A))` B)) e. (span` {((proj` (_|_` A))` B)}) /\ (y +h (w .h B)) = ((y +h (w .h ((proj` A)` B))) +h (w .h ((proj` (_|_` A))` B)))) -> E.v e. A E.u e. (span` {((proj` (_|_` A))` B)})(y +h (w .h B)) = (v +h u))
12		shaddcltOLD 9007	. . . . . . . . . . . . . . 15 |- (A e. SH -> ((y e. A /\ (w .h ((proj` A)` B)) e. A) -> (y +h (w .h ((proj` A)` B))) e. A))
13	1, 3	pjcli 9168	. . . . . . . . . . . . . . . 16 |- ((proj` A)` B) e. A
14		shmulcltOLD 9009	. . . . . . . . . . . . . . . . 17 |- (A e. SH -> ((w e. CC /\ ((proj` A)` B) e. A) -> (w .h ((proj` A)` B)) e. A))
15	2, 14	ax-mp 7	. . . . . . . . . . . . . . . 16 |- ((w e. CC /\ ((proj` A)` B) e. A) -> (w .h ((proj` A)` B)) e. A)
16	13, 15	mpan2 694	. . . . . . . . . . . . . . 15 |- (w e. CC -> (w .h ((proj` A)` B)) e. A)
17	12, 16	sylan2i 465	. . . . . . . . . . . . . 14 |- (A e. SH -> ((y e. A /\ w e. CC) -> (y +h (w .h ((proj` A)` B))) e. A))
18	2, 17	ax-mp 7	. . . . . . . . . . . . 13 |- ((y e. A /\ w e. CC) -> (y +h (w .h ((proj` A)` B))) e. A)
19	1	choccl 9101	. . . . . . . . . . . . . . . 16 |- (_|_` A) e. CH
20	19, 3	pjhcli 9169	. . . . . . . . . . . . . . 15 |- ((proj` (_|_` A))` B) e. H~
21		spansnmul 9403	. . . . . . . . . . . . . . 15 |- ((((proj` (_|_` A))` B) e. H~ /\ w e. CC) -> (w .h ((proj` (_|_` A))` B)) e. (span` {((proj` (_|_` A))` B)}))
22	20, 21	mpan 693	. . . . . . . . . . . . . 14 |- (w e. CC -> (w .h ((proj` (_|_` A))` B)) e. (span` {((proj` (_|_` A))` B)}))
23	22	adantl 388	. . . . . . . . . . . . 13 |- ((y e. A /\ w e. CC) -> (w .h ((proj` (_|_` A))` B)) e. (span` {((proj` (_|_` A))` B)}))
24	1, 3	pjhcli 9169	. . . . . . . . . . . . . . . . . 18 |- ((proj` A)` B) e. H~
25		ax-hvdistr1 8799	. . . . . . . . . . . . . . . . . 18 |- ((w e. CC /\ ((proj` A)` B) e. H~ /\ ((proj` (_|_` A))` B) e. H~) -> (w .h (((proj` A)` B) +h ((proj` (_|_` A))` B))) = ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B))))
26	24, 20, 25	mp3an23 905	. . . . . . . . . . . . . . . . 17 |- (w e. CC -> (w .h (((proj` A)` B) +h ((proj` (_|_` A))` B))) = ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B))))
27	1, 3	pjpj 9172	. . . . . . . . . . . . . . . . . 18 |- B = (((proj` A)` B) +h ((proj` (_|_` A))` B))
28	27	opreq2i 3957	. . . . . . . . . . . . . . . . 17 |- (w .h B) = (w .h (((proj` A)` B) +h ((proj` (_|_` A))` B)))
29	26, 28	syl5eq 1511	. . . . . . . . . . . . . . . 16 |- (w e. CC -> (w .h B) = ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B))))
30	29	adantl 388	. . . . . . . . . . . . . . 15 |- ((y e. A /\ w e. CC) -> (w .h B) = ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B))))
31	30	opreq2d 3961	. . . . . . . . . . . . . 14 |- ((y e. A /\ w e. CC) -> (y +h (w .h B)) = (y +h ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B)))))
32		ax-hvass 8793	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ (w .h ((proj` A)` B)) e. H~ /\ (w .h ((proj` (_|_` A))` B)) e. H~) -> ((y +h (w .h ((proj` A)` B))) +h (w .h ((proj` (_|_` A))` B))) = (y +h ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B)))))
33	32	3expb 832	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ ((w .h ((proj` A)` B)) e. H~ /\ (w .h ((proj` (_|_` A))` B)) e. H~)) -> ((y +h (w .h ((proj` A)` B))) +h (w .h ((proj` (_|_` A))` B))) = (y +h ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B)))))
34	1	chel 9023	. . . . . . . . . . . . . . 15 |- (y e. A -> y e. H~)
35		hvmulclt 8804	. . . . . . . . . . . . . . . . 17 |- ((w e. CC /\ ((proj` A)` B) e. H~) -> (w .h ((proj` A)` B)) e. H~)
36	24, 35	mpan2 694	. . . . . . . . . . . . . . . 16 |- (w e. CC -> (w .h ((proj` A)` B)) e. H~)
37		hvmulclt 8804	. . . . . . . . . . . . . . . . 17 |- ((w e. CC /\ ((proj` (_|_` A))` B) e. H~) -> (w .h ((proj` (_|_` A))` B)) e. H~)
38	20, 37	mpan2 694	. . . . . . . . . . . . . . . 16 |- (w e. CC -> (w .h ((proj` (_|_` A))` B)) e. H~)
39	36, 38	jca 288	. . . . . . . . . . . . . . 15 |- (w e. CC -> ((w .h ((proj` A)` B)) e. H~ /\ (w .h ((proj` (_|_` A))` B)) e. H~))
40	33, 34, 39	syl2an 454	. . . . . . . . . . . . . 14 |- ((y e. A /\ w e. CC) -> ((y +h (w .h ((proj` A)` B))) +h (w .h ((proj` (_|_` A))` B))) = (y +h ((w .h ((proj` A)` B)) +h (w .h ((proj` (_|_` A))` B)))))
41	31, 40	eqtr4d 1502	. . . . . . . . . . . . 13 |- ((y e. A /\ w e. CC) -> (y +h (w .h B)) = ((y +h (w .h ((proj` A)` B))) +h (w .h ((proj` (_|_` A))` B))))
42	11, 18, 23, 41	syl3anc 856	. . . . . . . . . . . 12 |- ((y e. A /\ w e. CC) -> E.v e. A E.u e. (span` {((proj` (_|_` A))` B)})(y +h (w .h B)) = (v +h u))
43		snssi 2457	. . . . . . . . . . . . . . 15 |- (((proj` (_|_` A))` B) e. H~ -> {((proj` (_|_` A))` B)} (_ H~)
44	20, 43	ax-mp 7	. . . . . . . . . . . . . 14 |- {((proj` (_|_` A))` B)} (_ H~
45		spanclt 9219	. . . . . . . . . . . . . 14 |- ({((proj` (_|_` A))` B)} (_ H~ -> (span` {((proj` (_|_` A))` B)}) e. SH)
46	44, 45	ax-mp 7	. . . . . . . . . . . . 13 |- (span` {((proj` (_|_` A))` B)}) e. SH
47	2, 46	shsel 9195	. . . . . . . . . . . 12 |- ((y +h (w .h B)) e. (A +H (span` {((proj` (_|_` A))` B)})) <-> E.v e. A E.u e. (span` {((proj` (_|_` A))` B)})(y +h (w .h B)) = (v +h u))
48	42, 47	sylibr 200	. . . . . . . . . . 11 |- ((y e. A /\ w e. CC) -> (y +h (w .h B)) e. (A +H (span` {((proj` (_|_` A))` B)})))
49		opreq2 3954	. . . . . . . . . . . . 13 |- (z