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 e. CH
sumdmdi.2 
|- B e. CH
Assertion sumdmdlem 
|- ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( ( B +H ( span ` { C } ) ) i^i A ) = ( B i^i A ) )

Proof

Step Hyp Ref Expression
1 sumdmdi.1 
 |-  A e. CH
2 sumdmdi.2 
 |-  B e. CH
3 elin 
 |-  ( y e. ( ( B +H ( span ` { C } ) ) i^i A ) <-> ( y e. ( B +H ( span ` { C } ) ) /\ y e. A ) )
4 2 chshii 
 |-  B e. SH
5 spansnsh 
 |-  ( C e. ~H -> ( span ` { C } ) e. SH )
6 shsel 
 |-  ( ( 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 ) ) )
7 4 5 6 sylancr 
 |-  ( C e. ~H -> ( y e. ( B +H ( span ` { C } ) ) <-> E. z e. B E. w e. ( span ` { C } ) y = ( z +h w ) ) )
8 1 cheli 
 |-  ( y e. A -> y e. ~H )
9 2 cheli 
 |-  ( z e. B -> z e. ~H )
10 elspansncl 
 |-  ( ( C e. ~H /\ w e. ( span ` { C } ) ) -> w e. ~H )
11 hvsubadd 
 |-  ( ( y e. ~H /\ z e. ~H /\ w e. ~H ) -> ( ( y -h z ) = w <-> ( z +h w ) = y ) )
12 eqcom 
 |-  ( ( z +h w ) = y <-> y = ( z +h w ) )
13 11 12 bitrdi 
 |-  ( ( y e. ~H /\ z e. ~H /\ w e. ~H ) -> ( ( y -h z ) = w <-> y = ( z +h w ) ) )
14 8 9 10 13 syl3an 
 |-  ( ( y e. A /\ z e. B /\ ( C e. ~H /\ w e. ( span ` { C } ) ) ) -> ( ( y -h z ) = w <-> y = ( z +h w ) ) )
15 14 3expa 
 |-  ( ( ( y e. A /\ z e. B ) /\ ( C e. ~H /\ w e. ( span ` { C } ) ) ) -> ( ( y -h z ) = w <-> y = ( z +h w ) ) )
16 1 chshii 
 |-  A e. SH
17 16 4 shsvsi 
 |-  ( ( y e. A /\ z e. B ) -> ( y -h z ) e. ( A +H B ) )
18 eleq1 
 |-  ( ( y -h z ) = w -> ( ( y -h z ) e. ( A +H B ) <-> w e. ( A +H B ) ) )
19 17 18 syl5ibcom 
 |-  ( ( y e. A /\ z e. B ) -> ( ( y -h z ) = w -> w e. ( A +H B ) ) )
20 19 adantr 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 16 4 shscli 
 |-  ( A +H B ) e. SH
27 elspansn5 
 |-  ( ( 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 
 |-  ( ( ( C e. ~H /\ -. C e. ( A +H B ) ) /\ ( w e. ( span ` { C } ) /\ w e. ( A +H B ) ) ) -> w = 0h )
29 28 exp32 
 |-  ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( w e. ( span ` { C } ) -> ( w e. ( A +H B ) -> w = 0h ) ) )
30 29 adantl 
 |-  ( ( ( 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 
 |-  ( ( ( 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 oveq2 
 |-  ( w = 0h -> ( z +h w ) = ( z +h 0h ) )
33 ax-hvaddid 
 |-  ( z e. ~H -> ( z +h 0h ) = z )
34 32 33 sylan9eqr 
 |-  ( ( z e. ~H /\ w = 0h ) -> ( z +h w ) = z )
35 9 34 sylan 
 |-  ( ( z e. B /\ w = 0h ) -> ( z +h w ) = z )
36 35 eqeq2d 
 |-  ( ( z e. B /\ w = 0h ) -> ( y = ( z +h w ) <-> y = z ) )
37 36 adantll 
 |-  ( ( ( y e. A /\ z e. B ) /\ w = 0h ) -> ( y = ( z +h w ) <-> y = z ) )
38 37 biimpac 
 |-  ( ( y = ( z +h w ) /\ ( ( y e. A /\ z e. B ) /\ w = 0h ) ) -> y = z )
39 eleq1 
 |-  ( y = z -> ( y e. B <-> z e. B ) )
40 39 biimparc 
 |-  ( ( z e. B /\ y = z ) -> y e. B )
41 elin 
 |-  ( y e. ( B i^i A ) <-> ( y e. B /\ y e. A ) )
42 41 biimpri 
 |-  ( ( y e. B /\ y e. A ) -> y e. ( B i^i A ) )
43 42 ancoms 
 |-  ( ( y e. A /\ y e. B ) -> y e. ( B i^i A ) )
44 40 43 sylan2 
 |-  ( ( y e. A /\ ( z e. B /\ y = z ) ) -> y e. ( B i^i A ) )
45 44 expr 
 |-  ( ( y e. A /\ z e. B ) -> ( y = z -> y e. ( B i^i A ) ) )
46 45 ad2antrl 
 |-  ( ( y = ( z +h w ) /\ ( ( y e. A /\ z e. B ) /\ w = 0h ) ) -> ( y = z -> y e. ( B i^i A ) ) )
47 38 46 mpd 
 |-  ( ( y = ( z +h w ) /\ ( ( y e. A /\ z e. B ) /\ w = 0h ) ) -> y e. ( B i^i A ) )
48 47 expr 
 |-  ( ( y = ( z +h w ) /\ ( y e. A /\ z e. B ) ) -> ( w = 0h -> y e. ( B i^i A ) ) )
49 48 a1d 
 |-  ( ( y = ( z +h w ) /\ ( y e. A /\ z e. B ) ) -> ( w e. ( span ` { C } ) -> ( w = 0h -> y e. ( B i^i A ) ) ) )
50 49 adantr 
 |-  ( ( ( 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 ) ) ) )
51 31 50 mpdd 
 |-  ( ( ( 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 ) ) )
52 51 ex 
 |-  ( ( 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 ) ) ) )
53 52 com23 
 |-  ( ( 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 ) ) ) )
54 53 exp32 
 |-  ( 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 ) ) ) ) ) )
55 54 com4l 
 |-  ( 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 ) ) ) ) ) )
56 55 imp4c 
 |-  ( 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 ) ) ) )
57 56 exp4a 
 |-  ( 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 com23 
 |-  ( y e. A -> ( C e. ~H -> ( ( ( z e. B /\ w e. ( span ` { C } ) ) /\ y = ( z +h w ) ) -> ( -. C e. ( A +H B ) -> y e. ( B i^i A ) ) ) ) )
59 58 com4l 
 |-  ( C e. ~H -> ( ( ( z e. B /\ w e. ( span ` { C } ) ) /\ y = ( z +h w ) ) -> ( -. C e. ( A +H B ) -> ( y e. A -> y e. ( B i^i A ) ) ) ) )
60 59 expd 
 |-  ( C e. ~H -> ( ( z e. B /\ w e. ( span ` { C } ) ) -> ( y = ( z +h w ) -> ( -. C e. ( A +H B ) -> ( y e. A -> y e. ( B i^i A ) ) ) ) ) )
61 60 rexlimdvv 
 |-  ( C e. ~H -> ( E. z e. B E. w e. ( span ` { C } ) y = ( z +h w ) -> ( -. C e. ( A +H B ) -> ( y e. A -> y e. ( B i^i A ) ) ) ) )
62 7 61 sylbid 
 |-  ( C e. ~H -> ( y e. ( B +H ( span ` { C } ) ) -> ( -. C e. ( A +H B ) -> ( y e. A -> y e. ( B i^i A ) ) ) ) )
63 62 com23 
 |-  ( C e. ~H -> ( -. C e. ( A +H B ) -> ( y e. ( B +H ( span ` { C } ) ) -> ( y e. A -> y e. ( B i^i A ) ) ) ) )
64 63 imp4b 
 |-  ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( ( y e. ( B +H ( span ` { C } ) ) /\ y e. A ) -> y e. ( B i^i A ) ) )
65 3 64 syl5bi 
 |-  ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( y e. ( ( B +H ( span ` { C } ) ) i^i A ) -> y e. ( B i^i A ) ) )
66 65 ssrdv 
 |-  ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( ( B +H ( span ` { C } ) ) i^i A ) C_ ( B i^i A ) )
67 shsub1 
 |-  ( ( B e. SH /\ ( span ` { C } ) e. SH ) -> B C_ ( B +H ( span ` { C } ) ) )
68 4 5 67 sylancr 
 |-  ( C e. ~H -> B C_ ( B +H ( span ` { C } ) ) )
69 68 ssrind 
 |-  ( C e. ~H -> ( B i^i A ) C_ ( ( B +H ( span ` { C } ) ) i^i A ) )
70 69 adantr 
 |-  ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( B i^i A ) C_ ( ( B +H ( span ` { C } ) ) i^i A ) )
71 66 70 eqssd 
 |-  ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( ( B +H ( span ` { C } ) ) i^i A ) = ( B i^i A ) )