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 biimtrid ⊢ 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