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⁡Cy=z+ℎw
7 4 5 6 sylancr ⊢C∈ℋ→y∈B+ℋspan⁡C↔∃z∈B∃w∈span⁡Cy=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⁡Cy=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