Metamath Proof Explorer

Theorem shscli

Description: Closure of subspace sum. (Contributed by NM, 15-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses shscl.1 
|- A e. SH
shscl.2 
|- B e. SH
Assertion shscli 
|- ( A +H B ) e. SH

Proof

Step Hyp Ref Expression
1 shscl.1 
 |-  A e. SH
2 shscl.2 
 |-  B e. SH
3 shsss 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) C_ ~H )
4 1 2 3 mp2an 
 |-  ( A +H B ) C_ ~H
5 sh0 
 |-  ( A e. SH -> 0h e. A )
6 1 5 ax-mp 
 |-  0h e. A
7 sh0 
 |-  ( B e. SH -> 0h e. B )
8 2 7 ax-mp 
 |-  0h e. B
9 ax-hv0cl 
 |-  0h e. ~H
10 9 hvaddid2i 
 |-  ( 0h +h 0h ) = 0h
11 10 eqcomi 
 |-  0h = ( 0h +h 0h )
12 rspceov 
 |-  ( ( 0h e. A /\ 0h e. B /\ 0h = ( 0h +h 0h ) ) -> E. x e. A E. y e. B 0h = ( x +h y ) )
13 6 8 11 12 mp3an 
 |-  E. x e. A E. y e. B 0h = ( x +h y )
14 1 2 shseli 
 |-  ( 0h e. ( A +H B ) <-> E. x e. A E. y e. B 0h = ( x +h y ) )
15 13 14 mpbir 
 |-  0h e. ( A +H B )
16 4 15 pm3.2i 
 |-  ( ( A +H B ) C_ ~H /\ 0h e. ( A +H B ) )
17 1 2 shseli 
 |-  ( x e. ( A +H B ) <-> E. z e. A E. w e. B x = ( z +h w ) )
18 1 2 shseli 
 |-  ( y e. ( A +H B ) <-> E. v e. A E. u e. B y = ( v +h u ) )
19 shaddcl 
 |-  ( ( A e. SH /\ z e. A /\ v e. A ) -> ( z +h v ) e. A )
20 1 19 mp3an1 
 |-  ( ( z e. A /\ v e. A ) -> ( z +h v ) e. A )
21 20 ad2ant2r 
 |-  ( ( ( z e. A /\ w e. B ) /\ ( v e. A /\ u e. B ) ) -> ( z +h v ) e. A )
22 21 ad2ant2r 
 |-  ( ( ( ( z e. A /\ w e. B ) /\ x = ( z +h w ) ) /\ ( ( v e. A /\ u e. B ) /\ y = ( v +h u ) ) ) -> ( z +h v ) e. A )
23 shaddcl 
 |-  ( ( B e. SH /\ w e. B /\ u e. B ) -> ( w +h u ) e. B )
24 2 23 mp3an1 
 |-  ( ( w e. B /\ u e. B ) -> ( w +h u ) e. B )
25 24 ad2ant2l 
 |-  ( ( ( z e. A /\ w e. B ) /\ ( v e. A /\ u e. B ) ) -> ( w +h u ) e. B )
26 25 ad2ant2r 
 |-  ( ( ( ( z e. A /\ w e. B ) /\ x = ( z +h w ) ) /\ ( ( v e. A /\ u e. B ) /\ y = ( v +h u ) ) ) -> ( w +h u ) e. B )
27 oveq12 
 |-  ( ( x = ( z +h w ) /\ y = ( v +h u ) ) -> ( x +h y ) = ( ( z +h w ) +h ( v +h u ) ) )
28 27 ad2ant2l 
 |-  ( ( ( ( z e. A /\ w e. B ) /\ x = ( z +h w ) ) /\ ( ( v e. A /\ u e. B ) /\ y = ( v +h u ) ) ) -> ( x +h y ) = ( ( z +h w ) +h ( v +h u ) ) )
29 1 sheli 
 |-  ( z e. A -> z e. ~H )
30 1 sheli 
 |-  ( v e. A -> v e. ~H )
31 29 30 anim12i 
 |-  ( ( z e. A /\ v e. A ) -> ( z e. ~H /\ v e. ~H ) )
32 2 sheli 
 |-  ( w e. B -> w e. ~H )
33 2 sheli 
 |-  ( u e. B -> u e. ~H )
34 32 33 anim12i 
 |-  ( ( w e. B /\ u e. B ) -> ( w e. ~H /\ u e. ~H ) )
35 hvadd4 
 |-  ( ( ( z e. ~H /\ v e. ~H ) /\ ( w e. ~H /\ u e. ~H ) ) -> ( ( z +h v ) +h ( w +h u ) ) = ( ( z +h w ) +h ( v +h u ) ) )
36 31 34 35 syl2an 
 |-  ( ( ( z e. A /\ v e. A ) /\ ( w e. B /\ u e. B ) ) -> ( ( z +h v ) +h ( w +h u ) ) = ( ( z +h w ) +h ( v +h u ) ) )
37 36 an4s 
 |-  ( ( ( z e. A /\ w e. B ) /\ ( v e. A /\ u e. B ) ) -> ( ( z +h v ) +h ( w +h u ) ) = ( ( z +h w ) +h ( v +h u ) ) )
38 37 ad2ant2r 
 |-  ( ( ( ( z e. A /\ w e. B ) /\ x = ( z +h w ) ) /\ ( ( v e. A /\ u e. B ) /\ y = ( v +h u ) ) ) -> ( ( z +h v ) +h ( w +h u ) ) = ( ( z +h w ) +h ( v +h u ) ) )
39 28 38 eqtr4d 
 |-  ( ( ( ( z e. A /\ w e. B ) /\ x = ( z +h w ) ) /\ ( ( v e. A /\ u e. B ) /\ y = ( v +h u ) ) ) -> ( x +h y ) = ( ( z +h v ) +h ( w +h u ) ) )
40 rspceov 
 |-  ( ( ( z +h v ) e. A /\ ( w +h u ) e. B /\ ( x +h y ) = ( ( z +h v ) +h ( w +h u ) ) ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) )
41 22 26 39 40 syl3anc 
 |-  ( ( ( ( z e. A /\ w e. B ) /\ x = ( z +h w ) ) /\ ( ( v e. A /\ u e. B ) /\ y = ( v +h u ) ) ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) )
42 41 ancoms 
 |-  ( ( ( ( v e. A /\ u e. B ) /\ y = ( v +h u ) ) /\ ( ( z e. A /\ w e. B ) /\ x = ( z +h w ) ) ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) )
43 42 exp43 
 |-  ( ( v e. A /\ u e. B ) -> ( y = ( v +h u ) -> ( ( z e. A /\ w e. B ) -> ( x = ( z +h w ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) ) ) ) )
44 43 rexlimivv 
 |-  ( E. v e. A E. u e. B y = ( v +h u ) -> ( ( z e. A /\ w e. B ) -> ( x = ( z +h w ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) ) ) )
45 44 com3l 
 |-  ( ( z e. A /\ w e. B ) -> ( x = ( z +h w ) -> ( E. v e. A E. u e. B y = ( v +h u ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) ) ) )
46 45 rexlimivv 
 |-  ( E. z e. A E. w e. B x = ( z +h w ) -> ( E. v e. A E. u e. B y = ( v +h u ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) ) )
47 46 imp 
 |-  ( ( E. z e. A E. w e. B x = ( z +h w ) /\ E. v e. A E. u e. B y = ( v +h u ) ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) )
48 17 18 47 syl2anb 
 |-  ( ( x e. ( A +H B ) /\ y e. ( A +H B ) ) -> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) )
49 1 2 shseli 
 |-  ( ( x +h y ) e. ( A +H B ) <-> E. f e. A E. g e. B ( x +h y ) = ( f +h g ) )
50 48 49 sylibr 
 |-  ( ( x e. ( A +H B ) /\ y e. ( A +H B ) ) -> ( x +h y ) e. ( A +H B ) )
51 50 rgen2 
 |-  A. x e. ( A +H B ) A. y e. ( A +H B ) ( x +h y ) e. ( A +H B )
52 shmulcl 
 |-  ( ( A e. SH /\ x e. CC /\ v e. A ) -> ( x .h v ) e. A )
53 1 52 mp3an1 
 |-  ( ( x e. CC /\ v e. A ) -> ( x .h v ) e. A )
54 53 adantrr 
 |-  ( ( x e. CC /\ ( v e. A /\ ( u e. B /\ y = ( v +h u ) ) ) ) -> ( x .h v ) e. A )
55 shmulcl 
 |-  ( ( B e. SH /\ x e. CC /\ u e. B ) -> ( x .h u ) e. B )
56 2 55 mp3an1 
 |-  ( ( x e. CC /\ u e. B ) -> ( x .h u ) e. B )
57 56 adantrr 
 |-  ( ( x e. CC /\ ( u e. B /\ y = ( v +h u ) ) ) -> ( x .h u ) e. B )
58 57 adantrl 
 |-  ( ( x e. CC /\ ( v e. A /\ ( u e. B /\ y = ( v +h u ) ) ) ) -> ( x .h u ) e. B )
59 oveq2 
 |-  ( y = ( v +h u ) -> ( x .h y ) = ( x .h ( v +h u ) ) )
60 59 adantl 
 |-  ( ( u e. B /\ y = ( v +h u ) ) -> ( x .h y ) = ( x .h ( v +h u ) ) )
61 60 ad2antll 
 |-  ( ( x e. CC /\ ( v e. A /\ ( u e. B /\ y = ( v +h u ) ) ) ) -> ( x .h y ) = ( x .h ( v +h u ) ) )
62 id 
 |-  ( x e. CC -> x e. CC )
63 ax-hvdistr1 
 |-  ( ( x e. CC /\ v e. ~H /\ u e. ~H ) -> ( x .h ( v +h u ) ) = ( ( x .h v ) +h ( x .h u ) ) )
64 62 30 33 63 syl3an 
 |-  ( ( x e. CC /\ v e. A /\ u e. B ) -> ( x .h ( v +h u ) ) = ( ( x .h v ) +h ( x .h u ) ) )
65 64 3expb 
 |-  ( ( x e. CC /\ ( v e. A /\ u e. B ) ) -> ( x .h ( v +h u ) ) = ( ( x .h v ) +h ( x .h u ) ) )
66 65 adantrrr 
 |-  ( ( x e. CC /\ ( v e. A /\ ( u e. B /\ y = ( v +h u ) ) ) ) -> ( x .h ( v +h u ) ) = ( ( x .h v ) +h ( x .h u ) ) )
67 61 66 eqtrd 
 |-  ( ( x e. CC /\ ( v e. A /\ ( u e. B /\ y = ( v +h u ) ) ) ) -> ( x .h y ) = ( ( x .h v ) +h ( x .h u ) ) )
68 rspceov 
 |-  ( ( ( x .h v ) e. A /\ ( x .h u ) e. B /\ ( x .h y ) = ( ( x .h v ) +h ( x .h u ) ) ) -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) )
69 54 58 67 68 syl3anc 
 |-  ( ( x e. CC /\ ( v e. A /\ ( u e. B /\ y = ( v +h u ) ) ) ) -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) )
70 69 ancoms 
 |-  ( ( ( v e. A /\ ( u e. B /\ y = ( v +h u ) ) ) /\ x e. CC ) -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) )
71 70 exp42 
 |-  ( v e. A -> ( u e. B -> ( y = ( v +h u ) -> ( x e. CC -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) ) ) ) )
72 71 imp 
 |-  ( ( v e. A /\ u e. B ) -> ( y = ( v +h u ) -> ( x e. CC -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) ) ) )
73 72 rexlimivv 
 |-  ( E. v e. A E. u e. B y = ( v +h u ) -> ( x e. CC -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) ) )
74 73 impcom 
 |-  ( ( x e. CC /\ E. v e. A E. u e. B y = ( v +h u ) ) -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) )
75 18 74 sylan2b 
 |-  ( ( x e. CC /\ y e. ( A +H B ) ) -> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) )
76 1 2 shseli 
 |-  ( ( x .h y ) e. ( A +H B ) <-> E. f e. A E. g e. B ( x .h y ) = ( f +h g ) )
77 75 76 sylibr 
 |-  ( ( x e. CC /\ y e. ( A +H B ) ) -> ( x .h y ) e. ( A +H B ) )
78 77 rgen2 
 |-  A. x e. CC A. y e. ( A +H B ) ( x .h y ) e. ( A +H B )
79 51 78 pm3.2i 
 |-  ( A. x e. ( A +H B ) A. y e. ( A +H B ) ( x +h y ) e. ( A +H B ) /\ A. x e. CC A. y e. ( A +H B ) ( x .h y ) e. ( A +H B ) )
80 issh2 
 |-  ( ( A +H B ) e. SH <-> ( ( ( A +H B ) C_ ~H /\ 0h e. ( A +H B ) ) /\ ( A. x e. ( A +H B ) A. y e. ( A +H B ) ( x +h y ) e. ( A +H B ) /\ A. x e. CC A. y e. ( A +H B ) ( x .h y ) e. ( A +H B ) ) ) )
81 16 79 80 mpbir2an 
 |-  ( A +H B ) e. SH