Metamath Proof Explorer

Theorem normcan

Description: Cancellation-type law that "extracts" a vector A from its inner product with a proportional vector B . (Contributed by NM, 18-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion normcan 
|- ( ( B e. ~H /\ B =/= 0h /\ A e. ( span ` { B } ) ) -> ( ( ( A .ih B ) / ( ( normh ` B ) ^ 2 ) ) .h B ) = A )

Proof

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 )