Step |
Hyp |
Ref |
Expression |
1 |
|
elspansn |
|- ( B e. ~H -> ( A e. ( span ` { B } ) <-> E. x e. CC A = ( x .h B ) ) ) |
2 |
1
|
adantr |
|- ( ( B e. ~H /\ B =/= 0h ) -> ( A e. ( span ` { B } ) <-> E. x e. CC A = ( x .h B ) ) ) |
3 |
|
oveq1 |
|- ( A = ( x .h B ) -> ( A .ih B ) = ( ( x .h B ) .ih B ) ) |
4 |
|
simpr |
|- ( ( B e. ~H /\ x e. CC ) -> x e. CC ) |
5 |
|
simpl |
|- ( ( B e. ~H /\ x e. CC ) -> B e. ~H ) |
6 |
|
ax-his3 |
|- ( ( x e. CC /\ B e. ~H /\ B e. ~H ) -> ( ( x .h B ) .ih B ) = ( x x. ( B .ih B ) ) ) |
7 |
4 5 5 6
|
syl3anc |
|- ( ( B e. ~H /\ x e. CC ) -> ( ( x .h B ) .ih B ) = ( x x. ( B .ih B ) ) ) |
8 |
3 7
|
sylan9eqr |
|- ( ( ( B e. ~H /\ x e. CC ) /\ A = ( x .h B ) ) -> ( A .ih B ) = ( x x. ( B .ih B ) ) ) |
9 |
|
normsq |
|- ( B e. ~H -> ( ( normh ` B ) ^ 2 ) = ( B .ih B ) ) |
10 |
9
|
ad2antrr |
|- ( ( ( B e. ~H /\ x e. CC ) /\ A = ( x .h B ) ) -> ( ( normh ` B ) ^ 2 ) = ( B .ih B ) ) |
11 |
8 10
|
oveq12d |
|- ( ( ( B e. ~H /\ x e. CC ) /\ A = ( x .h B ) ) -> ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) = ( ( x x. ( B .ih B ) ) / ( B .ih B ) ) ) |
12 |
11
|
adantllr |
|- ( ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) /\ A = ( x .h B ) ) -> ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) = ( ( x x. ( B .ih B ) ) / ( B .ih B ) ) ) |
13 |
|
simpr |
|- ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) -> x e. CC ) |
14 |
|
hicl |
|- ( ( B e. ~H /\ B e. ~H ) -> ( B .ih B ) e. CC ) |
15 |
14
|
anidms |
|- ( B e. ~H -> ( B .ih B ) e. CC ) |
16 |
15
|
ad2antrr |
|- ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) -> ( B .ih B ) e. CC ) |
17 |
|
his6 |
|- ( B e. ~H -> ( ( B .ih B ) = 0 <-> B = 0h ) ) |
18 |
17
|
necon3bid |
|- ( B e. ~H -> ( ( B .ih B ) =/= 0 <-> B =/= 0h ) ) |
19 |
18
|
biimpar |
|- ( ( B e. ~H /\ B =/= 0h ) -> ( B .ih B ) =/= 0 ) |
20 |
19
|
adantr |
|- ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) -> ( B .ih B ) =/= 0 ) |
21 |
13 16 20
|
divcan4d |
|- ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) -> ( ( x x. ( B .ih B ) ) / ( B .ih B ) ) = x ) |
22 |
21
|
adantr |
|- ( ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) /\ A = ( x .h B ) ) -> ( ( x x. ( B .ih B ) ) / ( B .ih B ) ) = x ) |
23 |
12 22
|
eqtrd |
|- ( ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) /\ A = ( x .h B ) ) -> ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) = x ) |
24 |
23
|
oveq1d |
|- ( ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) /\ A = ( x .h B ) ) -> ( ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) .h B ) = ( x .h B ) ) |
25 |
|
simpr |
|- ( ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) /\ A = ( x .h B ) ) -> A = ( x .h B ) ) |
26 |
24 25
|
eqtr4d |
|- ( ( ( ( B e. ~H /\ B =/= 0h ) /\ x e. CC ) /\ A = ( x .h B ) ) -> ( ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) .h B ) = A ) |
27 |
26
|
rexlimdva2 |
|- ( ( B e. ~H /\ B =/= 0h ) -> ( E. x e. CC A = ( x .h B ) -> ( ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) .h B ) = A ) ) |
28 |
2 27
|
sylbid |
|- ( ( B e. ~H /\ B =/= 0h ) -> ( A e. ( span ` { B } ) -> ( ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) .h B ) = A ) ) |
29 |
28
|
3impia |
|- ( ( B e. ~H /\ B =/= 0h /\ A e. ( span ` { B } ) ) -> ( ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) .h B ) = A ) |