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 )