Theorem sumdmdlem 10340

Description: Lemma for sumdmd 10342. 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 9479	. . . . . . . 8 |- (C e. H~ -> (span` {C}) e. SH)
2		sumdmdi.2	. . . . . . . . . 10 |- B e. CH
3	2	chshi 9092	. . . . . . . . 9 |- B e. SH
4		shselt 9273	. . . . . . . . 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 +h w)))
5	3, 4	mpan 697	. . . . . . . 8 |- ((span` {C}) e. SH -> (y e. (B +H (span` {C})) <-> E.z e. B E.w e. (span` {C})y = (z +h w)))
6	1, 5	syl 10	. . . . . . 7 |- (C e. H~ -> (y e. (B +H (span` {C})) <-> E.z e. B E.w e. (span` {C})y = (z +h w)))
7		hvsubaddt 8939	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. H~ /\ z e. H~ /\ w e. H~) -> ((y -h z) = w <-> (z +h w) = y))
8		eqcom 1480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z +h w) = y <-> y = (z +h w))
9	7, 8	syl6bb 538	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. H~ /\ z e. H~ /\ w e. H~) -> ((y -h z) = w <-> y = (z +h w)))
10		sumdmdi.1	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- A e. CH
11	10	chel 9097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. A -> y e. H~)
12	2	chel 9097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. B -> z e. H~)
13		elspansnclt 9483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((C e. H~ /\ w e. (span` {C})) -> w e. H~)
14	9, 11, 12, 13	syl3an 870	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. A /\ z e. B /\ (C e. H~ /\ w e. (span` {C}))) -> ((y -h z) = w <-> y = (z +h w)))
15	14	3expa 835	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. A /\ z e. B) /\ (C e. H~ /\ w e. (span` {C}))) -> ((y -h z) = w <-> y = (z +h w)))
16		eleq1 1537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y -h z) = w -> ((y -h z) e. (A +H B) <-> w e. (A +H B)))
17	10	chshi 9092	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- A e. SH
18	17, 3	shsvs 9331	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. A /\ z e. B) -> (y -h z) e. (A +H B))
19	16, 18	syl5cbi 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. A /\ z e. B) -> ((y -h z) = w -> w e. (A +H B)))
20	19	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. A /\ z e. B) /\ (C e. H~ /\ w e. (span` {C}))) -> ((y -h z) = w -> w e. (A +H B)))
21	15, 20	sylbird 205	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((y e. A /\ z e. B) /\ (C e. H~ /\ w e. (span` {C}))) -> (y = (z +h w) -> w e. (A +H B)))
22	21	exp32 379	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. A /\ z e. B) -> (C e. H~ -> (w e. (span` {C}) -> (y = (z +h w) -> w e. (A +H B)))))
23	22	com4r 41	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (z +h w) -> ((y e. A /\ z e. B) -> (C e. H~ -> (w e. (span` {C}) -> w e. (A +H B)))))
24	23	imp31 362	. . . . . . . . . . . . . . . . . . . 20 |- (((y = (z +h w) /\ (y e. A /\ z e. B)) /\ C e. H~) -> (w e. (span` {C}) -> w e. (A +H B)))
25	24	adantrr 397	. . . . . . . . . . . . . . . . . . 19 |- (((y = (z +h w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> w e. (A +H B)))
26	17, 3	shscl 9276	. . . . . . . . . . . . . . . . . . . . . 22 |- (A +H B) e. SH
27		elspansn5t 9492	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A +H B) e. SH -> (((C e. H~ /\ -. C e. (A +H B)) /\ (w e. (span` {C}) /\ w e. (A +H B))) -> w = 0h))
28	26, 27	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- (((C e. H~ /\ -. C e. (A +H B)) /\ (w e. (span` {C}) /\ w e. (A +H B))) -> w = 0h)
29	28	exp32 379	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. H~ /\ -. C e. (A +H B)) -> (w e. (span` {C}) -> (w e. (A +H B) -> w = 0h)))
30	29	adantl 390	. . . . . . . . . . . . . . . . . . 19 |- (((y = (z +h 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 = 0h)))
31	25, 30	mpdd 46	. . . . . . . . . . . . . . . . . 18 |- (((y = (z +h w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> w = 0h))
32		opreq2 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = 0h -> (z +h w) = (z +h 0h))
33		ax-hvaddid 8869	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z e. H~ -> (z +h 0h) = z)
34	32, 33	sylan9eqr 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. H~ /\ w = 0h) -> (z +h w) = z)
35	34, 12	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z e. B /\ w = 0h) -> (z +h w) = z)
36	35	eqeq2d 1489	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z e. B /\ w = 0h) -> (y = (z +h w) <-> y = z))
37	36	adantll 394	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. A /\ z e. B) /\ w = 0h) -> (y = (z +h w) <-> y = z))
38	37	biimpac 420	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y = (z +h w) /\ ((y e. A /\ z e. B) /\ w = 0h)) -> y = z)
39		elin 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y e. (B i^i A) <-> (y e. B /\ y e. A))
40	39	biimpr 152	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. B /\ y e. A) -> y e. (B i^i A))
41	40	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. A /\ y e. B) -> y e. (B i^i A))
42		eleq1 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = z -> (y e. B <-> z e. B))
43	42	biimparc 421	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. B /\ y = z) -> y e. B)
44	41, 43	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. A /\ (z e. B /\ y = z)) -> y e. (B i^i A))
45	44	anassrs 443	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((y e. A /\ z e. B) /\ y = z) -> y e. (B i^i A))
46	45	ex 373	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. A /\ z e. B) -> (y = z -> y e. (B i^i A)))
47	46	ad2antrl 408	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y = (z +h w) /\ ((y e. A /\ z e. B) /\ w = 0h)) -> (y = z -> y e. (B i^i A)))
48	38, 47	mpd 26	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y = (z +h w) /\ ((y e. A /\ z e. B) /\ w = 0h)) -> y e. (B i^i A))
49	48	exp32 379	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (z +h w) -> ((y e. A /\ z e. B) -> (w = 0h -> y e. (B i^i A))))
50	49	imp 350	. . . . . . . . . . . . . . . . . . . 20 |- ((y = (z +h w) /\ (y e. A /\ z e. B)) -> (w = 0h -> y e. (B i^i A)))
51	50	a1d 12	. . . . . . . . . . . . . . . . . . 19 |- ((y = (z +h w) /\ (y e. A /\ z e. B)) -> (w e. (span` {C}) -> (w = 0h -> y e. (B i^i A))))
52	51	adantr 391	. . . . . . . . . . . . . . . . . 18 |- (((y = (z +h w) /\ (y e. A /\ z e. B)) /\ (C e. H~ /\ -. C e. (A +H B))) -> (w e. (span` {C}) -> (w = 0h -> y e. (B i^i A))))
53	31, 52	mpdd 46	. . . . . . . . . . . . . . . . 17 |- (((y = (z +h 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)))
54	53	ex 373	. . . . . . . . . . . . . . . 16 |- ((y = (z +h 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	com23 32	. . . . . . . . . . . . . . 15 |- ((y = (z +h 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))))
56	55	exp32 379	. . . . . . . . . . . . . 14 |- (y = (z +h 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	com4l 39	. . . . . . . . . . . . 13 |- (y e. A -> (z e. B -> (w e. (span` {C}) -> (y = (z +h w) -> ((C e. H~ /\ -. C e. (A +H B)) -> y e. (B i^i A))))))
58	57	imp4c 366	. . . . . . . . . . . 12 |- (