Metamath Proof Explorer


Theorem sumdmdlem

Description: Lemma for sumdmdi . The span of vector C not in the subspace sum is "trimmed off." (Contributed by NM, 18-Dec-2004) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 A C
sumdmdi.2 B C
Assertion sumdmdlem C ¬ C A + B B + span C A = B A

Proof

Step Hyp Ref Expression
1 sumdmdi.1 A C
2 sumdmdi.2 B C
3 elin y B + span C A y B + span C y A
4 2 chshii B S
5 spansnsh C span C S
6 shsel B S span C S y B + span C z B w span C y = z + w
7 4 5 6 sylancr C y B + span C z B w span C y = z + w
8 1 cheli y A y
9 2 cheli z B z
10 elspansncl C w span C w
11 hvsubadd y z w y - z = w z + w = y
12 eqcom z + w = y y = z + w
13 11 12 bitrdi y z w y - z = w y = z + w
14 8 9 10 13 syl3an y A z B C w span C y - z = w y = z + w
15 14 3expa y A z B C w span C y - z = w y = z + w
16 1 chshii A S
17 16 4 shsvsi y A z B y - z A + B
18 eleq1 y - z = w y - z A + B w A + B
19 17 18 syl5ibcom y A z B y - z = w w A + B
20 19 adantr y A z B C w span C y - z = w w A + B
21 15 20 sylbird y A z B C w span C y = z + w w A + B
22 21 exp32 y A z B C w span C y = z + w w A + B
23 22 com4r y = z + w y A z B C w span C w A + B
24 23 imp31 y = z + w y A z B C w span C w A + B
25 24 adantrr y = z + w y A z B C ¬ C A + B w span C w A + B
26 16 4 shscli A + B S
27 elspansn5 A + B S C ¬ C A + B w span C w A + B w = 0
28 26 27 ax-mp C ¬ C A + B w span C w A + B w = 0
29 28 exp32 C ¬ C A + B w span C w A + B w = 0
30 29 adantl y = z + w y A z B C ¬ C A + B w span C w A + B w = 0
31 25 30 mpdd y = z + w y A z B C ¬ C A + B w span C w = 0
32 oveq2 w = 0 z + w = z + 0
33 ax-hvaddid z z + 0 = z
34 32 33 sylan9eqr z w = 0 z + w = z
35 9 34 sylan z B w = 0 z + w = z
36 35 eqeq2d z B w = 0 y = z + w y = z
37 36 adantll y A z B w = 0 y = z + w y = z
38 37 biimpac y = z + w y A z B w = 0 y = z
39 eleq1 y = z y B z B
40 39 biimparc z B y = z y B
41 elin y B A y B y A
42 41 biimpri y B y A y B A
43 42 ancoms y A y B y B A
44 40 43 sylan2 y A z B y = z y B A
45 44 expr y A z B y = z y B A
46 45 ad2antrl y = z + w y A z B w = 0 y = z y B A
47 38 46 mpd y = z + w y A z B w = 0 y B A
48 47 expr y = z + w y A z B w = 0 y B A
49 48 a1d y = z + w y A z B w span C w = 0 y B A
50 49 adantr y = z + w y A z B C ¬ C A + B w span C w = 0 y B A
51 31 50 mpdd y = z + w y A z B C ¬ C A + B w span C y B A
52 51 ex y = z + w y A z B C ¬ C A + B w span C y B A
53 52 com23 y = z + w y A z B w span C C ¬ C A + B y B A
54 53 exp32 y = z + w y A z B w span C C ¬ C A + B y B A
55 54 com4l y A z B w span C y = z + w C ¬ C A + B y B A
56 55 imp4c y A z B w span C y = z + w C ¬ C A + B y B A
57 56 exp4a y A z B w span C y = z + w C ¬ C A + B y B A
58 57 com23 y A C z B w span C y = z + w ¬ C A + B y B A
59 58 com4l C z B w span C y = z + w ¬ C A + B y A y B A
60 59 expd C z B w span C y = z + w ¬ C A + B y A y B A
61 60 rexlimdvv C z B w span C y = z + w ¬ C A + B y A y B A
62 7 61 sylbid C y B + span C ¬ C A + B y A y B A
63 62 com23 C ¬ C A + B y B + span C y A y B A
64 63 imp4b C ¬ C A + B y B + span C y A y B A
65 3 64 syl5bi C ¬ C A + B y B + span C A y B A
66 65 ssrdv C ¬ C A + B B + span C A B A
67 shsub1 B S span C S B B + span C
68 4 5 67 sylancr C B B + span C
69 68 ssrind C B A B + span C A
70 69 adantr C ¬ C A + B B A B + span C A
71 66 70 eqssd C ¬ C A + B B + span C A = B A