Metamath Proof Explorer

Theorem shsel3

Description: Membership in the subspace sum of two Hilbert subspaces, using vector subtraction. (Contributed by NM, 20-Jan-2007) (New usage is discouraged.)

Ref Expression
Assertion shsel3 
|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x -h y ) ) )

Proof

Step Hyp Ref Expression
1 shsel 
 |-  ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> E. x e. A E. z e. B C = ( x +h z ) ) )
2 id 
 |-  ( C = ( x +h z ) -> C = ( x +h z ) )
3 shel 
 |-  ( ( A e. SH /\ x e. A ) -> x e. ~H )
4 shel 
 |-  ( ( B e. SH /\ z e. B ) -> z e. ~H )
5 hvaddsubval 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( x +h z ) = ( x -h ( -u 1 .h z ) ) )
6 3 4 5 syl2an 
 |-  ( ( ( A e. SH /\ x e. A ) /\ ( B e. SH /\ z e. B ) ) -> ( x +h z ) = ( x -h ( -u 1 .h z ) ) )
7 6 an4s 
 |-  ( ( ( A e. SH /\ B e. SH ) /\ ( x e. A /\ z e. B ) ) -> ( x +h z ) = ( x -h ( -u 1 .h z ) ) )
8 7 anassrs 
 |-  ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ z e. B ) -> ( x +h z ) = ( x -h ( -u 1 .h z ) ) )
9 2 8 sylan9eqr 
 |-  ( ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ z e. B ) /\ C = ( x +h z ) ) -> C = ( x -h ( -u 1 .h z ) ) )
10 neg1cn 
 |-  -u 1 e. CC
11 shmulcl 
 |-  ( ( B e. SH /\ -u 1 e. CC /\ z e. B ) -> ( -u 1 .h z ) e. B )
12 10 11 mp3an2 
 |-  ( ( B e. SH /\ z e. B ) -> ( -u 1 .h z ) e. B )
13 12 adantll 
 |-  ( ( ( A e. SH /\ B e. SH ) /\ z e. B ) -> ( -u 1 .h z ) e. B )
14 13 adantlr 
 |-  ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ z e. B ) -> ( -u 1 .h z ) e. B )
15 oveq2 
 |-  ( y = ( -u 1 .h z ) -> ( x -h y ) = ( x -h ( -u 1 .h z ) ) )
16 15 rspceeqv 
 |-  ( ( ( -u 1 .h z ) e. B /\ C = ( x -h ( -u 1 .h z ) ) ) -> E. y e. B C = ( x -h y ) )
17 14 16 sylan 
 |-  ( ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ z e. B ) /\ C = ( x -h ( -u 1 .h z ) ) ) -> E. y e. B C = ( x -h y ) )
18 9 17 syldan 
 |-  ( ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ z e. B ) /\ C = ( x +h z ) ) -> E. y e. B C = ( x -h y ) )
19 18 rexlimdva2 
 |-  ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) -> ( E. z e. B C = ( x +h z ) -> E. y e. B C = ( x -h y ) ) )
20 id 
 |-  ( C = ( x -h y ) -> C = ( x -h y ) )
21 shel 
 |-  ( ( B e. SH /\ y e. B ) -> y e. ~H )
22 hvsubval 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x -h y ) = ( x +h ( -u 1 .h y ) ) )
23 3 21 22 syl2an 
 |-  ( ( ( A e. SH /\ x e. A ) /\ ( B e. SH /\ y e. B ) ) -> ( x -h y ) = ( x +h ( -u 1 .h y ) ) )
24 23 an4s 
 |-  ( ( ( A e. SH /\ B e. SH ) /\ ( x e. A /\ y e. B ) ) -> ( x -h y ) = ( x +h ( -u 1 .h y ) ) )
25 24 anassrs 
 |-  ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ y e. B ) -> ( x -h y ) = ( x +h ( -u 1 .h y ) ) )
26 20 25 sylan9eqr 
 |-  ( ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ y e. B ) /\ C = ( x -h y ) ) -> C = ( x +h ( -u 1 .h y ) ) )
27 shmulcl 
 |-  ( ( B e. SH /\ -u 1 e. CC /\ y e. B ) -> ( -u 1 .h y ) e. B )
28 10 27 mp3an2 
 |-  ( ( B e. SH /\ y e. B ) -> ( -u 1 .h y ) e. B )
29 28 adantll 
 |-  ( ( ( A e. SH /\ B e. SH ) /\ y e. B ) -> ( -u 1 .h y ) e. B )
30 29 adantlr 
 |-  ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ y e. B ) -> ( -u 1 .h y ) e. B )
31 oveq2 
 |-  ( z = ( -u 1 .h y ) -> ( x +h z ) = ( x +h ( -u 1 .h y ) ) )
32 31 rspceeqv 
 |-  ( ( ( -u 1 .h y ) e. B /\ C = ( x +h ( -u 1 .h y ) ) ) -> E. z e. B C = ( x +h z ) )
33 30 32 sylan 
 |-  ( ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ y e. B ) /\ C = ( x +h ( -u 1 .h y ) ) ) -> E. z e. B C = ( x +h z ) )
34 26 33 syldan 
 |-  ( ( ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) /\ y e. B ) /\ C = ( x -h y ) ) -> E. z e. B C = ( x +h z ) )
35 34 rexlimdva2 
 |-  ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) -> ( E. y e. B C = ( x -h y ) -> E. z e. B C = ( x +h z ) ) )
36 19 35 impbid 
 |-  ( ( ( A e. SH /\ B e. SH ) /\ x e. A ) -> ( E. z e. B C = ( x +h z ) <-> E. y e. B C = ( x -h y ) ) )
37 36 rexbidva 
 |-  ( ( A e. SH /\ B e. SH ) -> ( E. x e. A E. z e. B C = ( x +h z ) <-> E. x e. A E. y e. B C = ( x -h y ) ) )
38 1 37 bitrd 
 |-  ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x -h y ) ) )