Metamath Proof Explorer

Theorem spanunsni

Description: The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses spanunsn.1 
|- A e. CH
spanunsn.2 
|- B e. ~H
Assertion spanunsni 
|- ( span ` ( A u. { B } ) ) = ( span ` ( A u. { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )

Proof

Step Hyp Ref Expression
1 spanunsn.1 
 |-  A e. CH
2 spanunsn.2 
 |-  B e. ~H
3 1 chshii 
 |-  A e. SH
4 snssi 
 |-  ( B e. ~H -> { B } C_ ~H )
5 spancl 
 |-  ( { B } C_ ~H -> ( span ` { B } ) e. SH )
6 2 4 5 mp2b 
 |-  ( span ` { B } ) e. SH
7 3 6 shseli 
 |-  ( x e. ( A +H ( span ` { B } ) ) <-> E. y e. A E. z e. ( span ` { B } ) x = ( y +h z ) )
8 2 elspansni 
 |-  ( z e. ( span ` { B } ) <-> E. w e. CC z = ( w .h B ) )
9 1 2 pjclii 
 |-  ( ( projh ` A ) ` B ) e. A
10 shmulcl 
 |-  ( ( A e. SH /\ w e. CC /\ ( ( projh ` A ) ` B ) e. A ) -> ( w .h ( ( projh ` A ) ` B ) ) e. A )
11 3 9 10 mp3an13 
 |-  ( w e. CC -> ( w .h ( ( projh ` A ) ` B ) ) e. A )
12 shaddcl 
 |-  ( ( A e. SH /\ y e. A /\ ( w .h ( ( projh ` A ) ` B ) ) e. A ) -> ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) e. A )
13 11 12 syl3an3 
 |-  ( ( A e. SH /\ y e. A /\ w e. CC ) -> ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) e. A )
14 3 13 mp3an1 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) e. A )
15 1 choccli 
 |-  ( _|_ ` A ) e. CH
16 15 2 pjhclii 
 |-  ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H
17 spansnmul 
 |-  ( ( ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H /\ w e. CC ) -> ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
18 16 17 mpan 
 |-  ( w e. CC -> ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
19 18 adantl 
 |-  ( ( y e. A /\ w e. CC ) -> ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
20 1 2 pjpji 
 |-  B = ( ( ( projh ` A ) ` B ) +h ( ( projh ` ( _|_ ` A ) ) ` B ) )
21 20 oveq2i 
 |-  ( w .h B ) = ( w .h ( ( ( projh ` A ) ` B ) +h ( ( projh ` ( _|_ ` A ) ) ` B ) ) )
22 1 2 pjhclii 
 |-  ( ( projh ` A ) ` B ) e. ~H
23 ax-hvdistr1 
 |-  ( ( w e. CC /\ ( ( projh ` A ) ` B ) e. ~H /\ ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H ) -> ( w .h ( ( ( projh ` A ) ` B ) +h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
24 22 16 23 mp3an23 
 |-  ( w e. CC -> ( w .h ( ( ( projh ` A ) ` B ) +h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
25 21 24 eqtrid 
 |-  ( w e. CC -> ( w .h B ) = ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
26 25 adantl 
 |-  ( ( y e. A /\ w e. CC ) -> ( w .h B ) = ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
27 26 oveq2d 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h B ) ) = ( y +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
28 1 cheli 
 |-  ( y e. A -> y e. ~H )
29 hvmulcl 
 |-  ( ( w e. CC /\ ( ( projh ` A ) ` B ) e. ~H ) -> ( w .h ( ( projh ` A ) ` B ) ) e. ~H )
30 22 29 mpan2 
 |-  ( w e. CC -> ( w .h ( ( projh ` A ) ` B ) ) e. ~H )
31 hvmulcl 
 |-  ( ( w e. CC /\ ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H ) -> ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H )
32 16 31 mpan2 
 |-  ( w e. CC -> ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H )
33 30 32 jca 
 |-  ( w e. CC -> ( ( w .h ( ( projh ` A ) ` B ) ) e. ~H /\ ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H ) )
34 ax-hvass 
 |-  ( ( y e. ~H /\ ( w .h ( ( projh ` A ) ` B ) ) e. ~H /\ ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H ) -> ( ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( y +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
35 34 3expb 
 |-  ( ( y e. ~H /\ ( ( w .h ( ( projh ` A ) ` B ) ) e. ~H /\ ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H ) ) -> ( ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( y +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
36 28 33 35 syl2an 
 |-  ( ( y e. A /\ w e. CC ) -> ( ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( y +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
37 27 36 eqtr4d 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h B ) ) = ( ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
38 rspceov 
 |-  ( ( ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) e. A /\ ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) /\ ( y +h ( w .h B ) ) = ( ( y +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) -> E. v e. A E. u e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ( y +h ( w .h B ) ) = ( v +h u ) )
39 14 19 37 38 syl3anc 
 |-  ( ( y e. A /\ w e. CC ) -> E. v e. A E. u e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ( y +h ( w .h B ) ) = ( v +h u ) )
40 snssi 
 |-  ( ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H -> { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ~H )
41 spancl 
 |-  ( { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ~H -> ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) e. SH )
42 16 40 41 mp2b 
 |-  ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) e. SH
43 3 42 shseli 
 |-  ( ( y +h ( w .h B ) ) e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) <-> E. v e. A E. u e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ( y +h ( w .h B ) ) = ( v +h u ) )
44 39 43 sylibr 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h B ) ) e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
45 oveq2 
 |-  ( z = ( w .h B ) -> ( y +h z ) = ( y +h ( w .h B ) ) )
46 45 eqeq2d 
 |-  ( z = ( w .h B ) -> ( x = ( y +h z ) <-> x = ( y +h ( w .h B ) ) ) )
47 46 biimpa 
 |-  ( ( z = ( w .h B ) /\ x = ( y +h z ) ) -> x = ( y +h ( w .h B ) ) )
48 eleq1 
 |-  ( x = ( y +h ( w .h B ) ) -> ( x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) <-> ( y +h ( w .h B ) ) e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) ) )
49 48 biimparc 
 |-  ( ( ( y +h ( w .h B ) ) e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) /\ x = ( y +h ( w .h B ) ) ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
50 44 47 49 syl2an 
 |-  ( ( ( y e. A /\ w e. CC ) /\ ( z = ( w .h B ) /\ x = ( y +h z ) ) ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
51 50 exp43 
 |-  ( y e. A -> ( w e. CC -> ( z = ( w .h B ) -> ( x = ( y +h z ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) ) ) ) )
52 51 rexlimdv 
 |-  ( y e. A -> ( E. w e. CC z = ( w .h B ) -> ( x = ( y +h z ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) ) ) )
53 8 52 biimtrid 
 |-  ( y e. A -> ( z e. ( span ` { B } ) -> ( x = ( y +h z ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) ) ) )
54 53 rexlimdv 
 |-  ( y e. A -> ( E. z e. ( span ` { B } ) x = ( y +h z ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) ) )
55 54 rexlimiv 
 |-  ( E. y e. A E. z e. ( span ` { B } ) x = ( y +h z ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
56 7 55 sylbi 
 |-  ( x e. ( A +H ( span ` { B } ) ) -> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
57 3 42 shseli 
 |-  ( x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) <-> E. y e. A E. z e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) x = ( y +h z ) )
58 16 elspansni 
 |-  ( z e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) <-> E. w e. CC z = ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) )
59 negcl 
 |-  ( w e. CC -> -u w e. CC )
60 shmulcl 
 |-  ( ( A e. SH /\ -u w e. CC /\ ( ( projh ` A ) ` B ) e. A ) -> ( -u w .h ( ( projh ` A ) ` B ) ) e. A )
61 3 9 60 mp3an13 
 |-  ( -u w e. CC -> ( -u w .h ( ( projh ` A ) ` B ) ) e. A )
62 59 61 syl 
 |-  ( w e. CC -> ( -u w .h ( ( projh ` A ) ` B ) ) e. A )
63 shaddcl 
 |-  ( ( A e. SH /\ ( -u w .h ( ( projh ` A ) ` B ) ) e. A /\ y e. A ) -> ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) e. A )
64 62 63 syl3an2 
 |-  ( ( A e. SH /\ w e. CC /\ y e. A ) -> ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) e. A )
65 3 64 mp3an1 
 |-  ( ( w e. CC /\ y e. A ) -> ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) e. A )
66 65 ancoms 
 |-  ( ( y e. A /\ w e. CC ) -> ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) e. A )
67 spansnmul 
 |-  ( ( B e. ~H /\ w e. CC ) -> ( w .h B ) e. ( span ` { B } ) )
68 2 67 mpan 
 |-  ( w e. CC -> ( w .h B ) e. ( span ` { B } ) )
69 68 adantl 
 |-  ( ( y e. A /\ w e. CC ) -> ( w .h B ) e. ( span ` { B } ) )
70 hvm1neg 
 |-  ( ( w e. CC /\ ( ( projh ` A ) ` B ) e. ~H ) -> ( -u 1 .h ( w .h ( ( projh ` A ) ` B ) ) ) = ( -u w .h ( ( projh ` A ) ` B ) ) )
71 22 70 mpan2 
 |-  ( w e. CC -> ( -u 1 .h ( w .h ( ( projh ` A ) ` B ) ) ) = ( -u w .h ( ( projh ` A ) ` B ) ) )
72 71 oveq2d 
 |-  ( w e. CC -> ( ( w .h ( ( projh ` A ) ` B ) ) +h ( -u 1 .h ( w .h ( ( projh ` A ) ` B ) ) ) ) = ( ( w .h ( ( projh ` A ) ` B ) ) +h ( -u w .h ( ( projh ` A ) ` B ) ) ) )
73 hvnegid 
 |-  ( ( w .h ( ( projh ` A ) ` B ) ) e. ~H -> ( ( w .h ( ( projh ` A ) ` B ) ) +h ( -u 1 .h ( w .h ( ( projh ` A ) ` B ) ) ) ) = 0h )
74 30 73 syl 
 |-  ( w e. CC -> ( ( w .h ( ( projh ` A ) ` B ) ) +h ( -u 1 .h ( w .h ( ( projh ` A ) ` B ) ) ) ) = 0h )
75 hvmulcl 
 |-  ( ( -u w e. CC /\ ( ( projh ` A ) ` B ) e. ~H ) -> ( -u w .h ( ( projh ` A ) ` B ) ) e. ~H )
76 59 22 75 sylancl 
 |-  ( w e. CC -> ( -u w .h ( ( projh ` A ) ` B ) ) e. ~H )
77 ax-hvcom 
 |-  ( ( ( w .h ( ( projh ` A ) ` B ) ) e. ~H /\ ( -u w .h ( ( projh ` A ) ` B ) ) e. ~H ) -> ( ( w .h ( ( projh ` A ) ` B ) ) +h ( -u w .h ( ( projh ` A ) ` B ) ) ) = ( ( -u w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` A ) ` B ) ) ) )
78 30 76 77 syl2anc 
 |-  ( w e. CC -> ( ( w .h ( ( projh ` A ) ` B ) ) +h ( -u w .h ( ( projh ` A ) ` B ) ) ) = ( ( -u w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` A ) ` B ) ) ) )
79 72 74 78 3eqtr3d 
 |-  ( w e. CC -> 0h = ( ( -u w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` A ) ` B ) ) ) )
80 79 adantl 
 |-  ( ( y e. A /\ w e. CC ) -> 0h = ( ( -u w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` A ) ` B ) ) ) )
81 80 oveq1d 
 |-  ( ( y e. A /\ w e. CC ) -> ( 0h +h ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) = ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
82 hvaddcl 
 |-  ( ( y e. ~H /\ ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H ) -> ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) e. ~H )
83 28 32 82 syl2an 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) e. ~H )
84 hvaddlid 
 |-  ( ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) e. ~H -> ( 0h +h ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) = ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
85 83 84 syl 
 |-  ( ( y e. A /\ w e. CC ) -> ( 0h +h ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) = ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
86 76 30 jca 
 |-  ( w e. CC -> ( ( -u w .h ( ( projh ` A ) ` B ) ) e. ~H /\ ( w .h ( ( projh ` A ) ` B ) ) e. ~H ) )
87 86 adantl 
 |-  ( ( y e. A /\ w e. CC ) -> ( ( -u w .h ( ( projh ` A ) ` B ) ) e. ~H /\ ( w .h ( ( projh ` A ) ` B ) ) e. ~H ) )
88 28 32 anim12i 
 |-  ( ( y e. A /\ w e. CC ) -> ( y e. ~H /\ ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H ) )
89 hvadd4 
 |-  ( ( ( ( -u w .h ( ( projh ` A ) ` B ) ) e. ~H /\ ( w .h ( ( projh ` A ) ` B ) ) e. ~H ) /\ ( y e. ~H /\ ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) e. ~H ) ) -> ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) = ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
90 87 88 89 syl2anc 
 |-  ( ( y e. A /\ w e. CC ) -> ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` A ) ` B ) ) ) +h ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) = ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
91 81 85 90 3eqtr3d 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
92 26 oveq2d 
 |-  ( ( y e. A /\ w e. CC ) -> ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) +h ( w .h B ) ) = ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) +h ( ( w .h ( ( projh ` A ) ` B ) ) +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
93 91 92 eqtr4d 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) +h ( w .h B ) ) )
94 rspceov 
 |-  ( ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) e. A /\ ( w .h B ) e. ( span ` { B } ) /\ ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( ( ( -u w .h ( ( projh ` A ) ` B ) ) +h y ) +h ( w .h B ) ) ) -> E. v e. A E. u e. ( span ` { B } ) ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( v +h u ) )
95 66 69 93 94 syl3anc 
 |-  ( ( y e. A /\ w e. CC ) -> E. v e. A E. u e. ( span ` { B } ) ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( v +h u ) )
96 3 6 shseli 
 |-  ( ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) e. ( A +H ( span ` { B } ) ) <-> E. v e. A E. u e. ( span ` { B } ) ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) = ( v +h u ) )
97 95 96 sylibr 
 |-  ( ( y e. A /\ w e. CC ) -> ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) e. ( A +H ( span ` { B } ) ) )
98 oveq2 
 |-  ( z = ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) -> ( y +h z ) = ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
99 98 eqeq2d 
 |-  ( z = ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) -> ( x = ( y +h z ) <-> x = ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) )
100 99 biimpa 
 |-  ( ( z = ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) /\ x = ( y +h z ) ) -> x = ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) )
101 eleq1 
 |-  ( x = ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) -> ( x e. ( A +H ( span ` { B } ) ) <-> ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) e. ( A +H ( span ` { B } ) ) ) )
102 101 biimparc 
 |-  ( ( ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) e. ( A +H ( span ` { B } ) ) /\ x = ( y +h ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) ) ) -> x e. ( A +H ( span ` { B } ) ) )
103 97 100 102 syl2an 
 |-  ( ( ( y e. A /\ w e. CC ) /\ ( z = ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) /\ x = ( y +h z ) ) ) -> x e. ( A +H ( span ` { B } ) ) )
104 103 exp43 
 |-  ( y e. A -> ( w e. CC -> ( z = ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) -> ( x = ( y +h z ) -> x e. ( A +H ( span ` { B } ) ) ) ) ) )
105 104 rexlimdv 
 |-  ( y e. A -> ( E. w e. CC z = ( w .h ( ( projh ` ( _|_ ` A ) ) ` B ) ) -> ( x = ( y +h z ) -> x e. ( A +H ( span ` { B } ) ) ) ) )
106 58 105 biimtrid 
 |-  ( y e. A -> ( z e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) -> ( x = ( y +h z ) -> x e. ( A +H ( span ` { B } ) ) ) ) )
107 106 rexlimdv 
 |-  ( y e. A -> ( E. z e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) x = ( y +h z ) -> x e. ( A +H ( span ` { B } ) ) ) )
108 107 rexlimiv 
 |-  ( E. y e. A E. z e. ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) x = ( y +h z ) -> x e. ( A +H ( span ` { B } ) ) )
109 57 108 sylbi 
 |-  ( x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) -> x e. ( A +H ( span ` { B } ) ) )
110 56 109 impbii 
 |-  ( x e. ( A +H ( span ` { B } ) ) <-> x e. ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
111 110 eqriv 
 |-  ( A +H ( span ` { B } ) ) = ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
112 1 chssii 
 |-  A C_ ~H
113 2 4 ax-mp 
 |-  { B } C_ ~H
114 112 113 spanuni 
 |-  ( span ` ( A u. { B } ) ) = ( ( span ` A ) +H ( span ` { B } ) )
115 spanid 
 |-  ( A e. SH -> ( span ` A ) = A )
116 3 115 ax-mp 
 |-  ( span ` A ) = A
117 116 oveq1i 
 |-  ( ( span ` A ) +H ( span ` { B } ) ) = ( A +H ( span ` { B } ) )
118 114 117 eqtri 
 |-  ( span ` ( A u. { B } ) ) = ( A +H ( span ` { B } ) )
119 16 40 ax-mp 
 |-  { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ~H
120 112 119 spanuni 
 |-  ( span ` ( A u. { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( ( span ` A ) +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
121 116 oveq1i 
 |-  ( ( span ` A ) +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
122 120 121 eqtri 
 |-  ( span ` ( A u. { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
123 111 118 122 3eqtr4i 
 |-  ( span ` ( A u. { B } ) ) = ( span ` ( A u. { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )