Theorem sumdmdlem 5786

Description: Lemma for sumdmd 5787. The span of vector C not in the subspace sum is "trimmed off."

Hypotheses

Ref	Expression
sumdmdi.1	|- A e. CH
sumdmdi.2	|- B e. CH

Assertion

Ref	Expression
sumdmdlem	|- ((C e. H~ /\ -. C e. (A +H B)) -> ((B +H (span` {C})) i^i A) = (B i^i A))

Proof of Theorem sumdmdlem

Step	Hyp	Ref	Expression
1		spansnsht 5466	. . . . . . . 8 |- (C e. H~ -> (span` {C}) e. SH)
2		sumdmdi.2	. . . . . . . . . 10 |- B e. CH
3	2	chshi 5132	. . . . . . . . 9 |- B e. SH
4		shselt 5280	. . . . . . . . 9 |- ((B e. SH /\ (span` {C}) e. SH) -> (y e. (B +H (span` {C})) <-> E.z e. B E.w e. (span` {C})y = (z +v w)))
5	3, 4	mpan 518	. . . . . . . 8 |- ((span` {C}) e. SH -> (y e. (B +H (span` {C})) <-> E.z e. B E.w e. (span` {C})y = (z +v w)))
6	1, 5	syl 12	. . . . . . 7 |- (C e. H~ -> (y e. (B +H (span` {C})) <-> E.z e. B E.w e. (span` {C})y = (z +v w)))
7		hvsubaddt 5042	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. H~ /\ z e. H~ /\ w e. H~) -> ((y -v z) = w <-> (z +v w) = y))
8		cleqcom 1103	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z +v w) = y <-> y = (z +v w))
9	7, 8	syl6bb 414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. H~ /\ z e. H~ /\ w e. H~) -> ((y -v z) = w <-> y = (z +v w)))
10		sumdmdi.1	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- A e. CH
11	10	chel 5137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. A -> y e. H~)
12	2	chel 5137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. B -> z e. H~)
13		elspansnclt 5470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((C e. H~ /\ w e. (span` {C})) -> w e. H~)
14	9, 11, 12, 13	syl3an 628	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. A /\ z e. B /\ (C e. H~ /\ w e. (span` {C}))) -> ((y -v z) = w <-> y = (z +v w)))
15	14	3expa 612	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. A /\ z e. B) /\ (C e. H~ /\ w e. (span` {C}))) -> ((y -v z) = w <-> y = (z +v w)))
16		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y -v z) = w -> ((y -v z) e. (A +H B) <-> w e. (A +H B)))
17	10	chshi 5132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- A e. SH
18	17, 3	shsvs 5337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. A /\ z e. B) -> (y -v z) e. (A +H B))
19	16, 18	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y -v z) = w -> ((y e. A /\ z e. B) -> w e. (A +H B)))
20	19	com12 13	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. A /\ z e. B) -> ((y -v z) = w -> w e. (A +H B)))
21	20	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. A /\ z e. B) /\ (C e. H~ /\ w e. (span` {C}))) -> ((y -v z) = w -> w e. (A +H B)))
22	15, 21	sylbird 180	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((y e. A /\ z e. B) /\ (C e. H~ /\ w e. (span` {C}))) -> (y = (z +v w) -> w e. (A +H B)))
23	22	exp32 294	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. A /\ z e. B) -> (C e. H~ -> (w e. (span` {C}) -> (y = (z +v w) -> w e. (A +H B)))))
24	23	com4r 41	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (z +v w) -> ((y e. A /\ z e. B) -> (C e. H~ -> (w e. (span` {C}) -> w e. (A +H B)))))
25	24	imp31 280	. . . . . . . . . . . . . . . . . . . 20 |- (((y = (z +v w) /\ (y e. A /\ z e. B)) /\ C e. H~) -> (w e. (span` {C}) -> w e. (A +H B)))
26	25	adantrr 312	. . . . . . . . . . . . . . . . . . 19 |- (((y = (z +v w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> w e. (A +H B)))
27	17, 3	shscl 5282	. . . . . . . . . . . . . . . . . . . . . 22 |- (A +H B) e. SH
28		elspansn5t 5479	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A +H B) e. SH -> (((C e. H~ /\ -. C e. (A +H B)) /\ (w e. (span` {C}) /\ w e. (A +H B))) -> w = 0v))
29	27, 28	ax-mp 6	. . . . . . . . . . . . . . . . . . . . 21 |- (((C e. H~ /\ -. C e. (A +H B)) /\ (w e. (span` {C}) /\ w e. (A +H B))) -> w = 0v)
30	29	exp32 294	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. H~ /\ -. C e. (A +H B)) -> (w e. (span` {C}) -> (w e. (A +H B) -> w = 0v)))
31	30	adantl 305	. . . . . . . . . . . . . . . . . . 19 |- (((y = (z +v w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> (w e. (A +H B) -> w = 0v)))
32	26, 31	mpdd 47	. . . . . . . . . . . . . . . . . 18 |- (((y = (z +v w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> w = 0v))
33		opreq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = 0v -> (z +v w) = (z +v 0v))
34		ax-hvaddid 4988	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z e. H~ -> (z +v 0v) = z)
35	33, 34	sylan9eqr 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. H~ /\ w = 0v) -> (z +v w) = z)
36	35, 12	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z e. B /\ w = 0v) -> (z +v w) = z)
37	36	cleq2d 1112	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z e. B /\ w = 0v) -> (y = (z +v w) <-> y = z))
38	37	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. A /\ z e. B) /\ w = 0v) -> (y = (z +v w) <-> y = z))
39	38	biimpac 326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y = (z +v w) /\ ((y e. A /\ z e. B) /\ w = 0v)) -> y = z)
40		elin 1635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y e. (B i^i A) <-> (y e. B /\ y e. A))
41	40	biimpr 134	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. B /\ y e. A) -> y e. (B i^i A))
42	41	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. A /\ y e. B) -> y e. (B i^i A))
43		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = z -> (y e. B <-> z e. B))
44	43	biimparc 327	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. B /\ y = z) -> y e. B)
45	42, 44	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. A /\ (z e. B /\ y = z)) -> y e. (B i^i A))
46	45	anassrs 338	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((y e. A /\ z e. B) /\ y = z) -> y e. (B i^i A))
47	46	exp 291	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. A /\ z e. B) -> (y = z -> y e. (B i^i A)))
48	47	ad2antrl 322	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y = (z +v w) /\ ((y e. A /\ z e. B) /\ w = 0v)) -> (y = z -> y e. (B i^i A)))
49	39, 48	mpd 46	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y = (z +v w) /\ ((y e. A /\ z e. B) /\ w = 0v)) -> y e. (B i^i A))
50	49	exp32 294	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (z +v w) -> ((y e. A /\ z e. B) -> (w = 0v -> y e. (B i^i A))))
51	50	imp 277	. . . . . . . . . . . . . . . . . . . 20 |- ((y = (z +v w) /\ (y e. A /\ z e. B)) -> (w = 0v -> y e. (B i^i A)))
52	51	a1d 14	. . . . . . . . . . . . . . . . . . 19 |- ((y = (z +v w) /\ (y e. A /\ z e. B)) -> (w e. (span` {C}) -> (w = 0v -> y e. (B i^i A))))
53	52	adantr 306	. . . . . . . . . . . . . . . . . 18 |- (((y = (z +v w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> (w = 0v -> y e. (B i^i A))))
54	32, 53	mpdd 47	. . . . . . . . . . . . . . . . 17 |- (((y = (z +v w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> y e. (B i^i A)))
55	54	exp 291	. . . . . . . . . . . . . . . 16 |- ((y = (z +v w) /\ (y e. A /\ z e. B)) -> ((C e. H~ /\ -. C e. (A +H B)) -> (w e. (span` {C}) -> y e. (B i^i A))))
56	55	com23 32	. . . . . . . . . . . . . . 15 |- ((y = (z +v w) /\ (y e. A /\ z e. B)) -> (w e. (span` {C}) -> ((C e. H~ /\ -. C e. (A +H B)) -> y e. (B i^i A))))
57	56	exp32 294	. . . . . . . . . . . . . 14 |- (y = (z +v w) -> (y e. A -> (z e. B -> (w e. (span` {C}) -> ((C e. H~ /\ -. C e. (A +H B)) -> y e. (B i^i A))))))
58	57	com4l 39	. . . . . . . . . . . . 13 |- (y e. A -> (z e. B -> (w e. (span` {C}) -> (y = (z +v w) -> ((C e. H~ /\ -. C e. (A +H B)) -> y e. (B i^i A))))))
59	58	imp4c 284	. . . . . . . . . . . 12 |- (y e. A -> (((z e. B /\ w e. (span` {C})) /\ y =