# 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}\in {\mathbf{C}}_{ℋ}$
sumdmdi.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion sumdmdlem ${⊢}\left({C}\in ℋ\wedge ¬{C}\in \left({A}{+}_{ℋ}{B}\right)\right)\to \left({B}{+}_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\cap {A}={B}\cap {A}$

### Proof

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