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∈ℋ∧B≠0ℎ∧A∈span⁡B→A⋅ihBnormℎ⁡B2⋅ℎB=A

Proof

Step Hyp Ref Expression
1 elspansn ⊢B∈ℋ→A∈span⁡B↔∃x∈ℂA=x⋅ℎB
2 1 adantr ⊢B∈ℋ∧B≠0ℎ→A∈span⁡B↔∃x∈ℂA=x⋅ℎB
3 oveq1 ⊢A=x⋅ℎB→A⋅ihB=x⋅ℎB⋅ihB
4 simpr ⊢B∈ℋ∧x∈ℂ→x∈ℂ
5 simpl ⊢B∈ℋ∧x∈ℂ→B∈ℋ
6 ax-his3 ⊢x∈ℂ∧B∈ℋ∧B∈ℋ→x⋅ℎB⋅ihB=x⁢B⋅ihB
7 4 5 5 6 syl3anc ⊢B∈ℋ∧x∈ℂ→x⋅ℎB⋅ihB=x⁢B⋅ihB
8 3 7 sylan9eqr ⊢B∈ℋ∧x∈ℂ∧A=x⋅ℎB→A⋅ihB=x⁢B⋅ihB
9 normsq ⊢B∈ℋ→normℎ⁡B2=B⋅ihB
10 9 ad2antrr ⊢B∈ℋ∧x∈ℂ∧A=x⋅ℎB→normℎ⁡B2=B⋅ihB
11 8 10 oveq12d ⊢B∈ℋ∧x∈ℂ∧A=x⋅ℎB→A⋅ihBnormℎ⁡B2=x⁢B⋅ihBB⋅ihB
12 11 adantllr ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ∧A=x⋅ℎB→A⋅ihBnormℎ⁡B2=x⁢B⋅ihBB⋅ihB
13 simpr ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ→x∈ℂ
14 hicl ⊢B∈ℋ∧B∈ℋ→B⋅ihB∈ℂ
15 14 anidms ⊢B∈ℋ→B⋅ihB∈ℂ
16 15 ad2antrr ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ→B⋅ihB∈ℂ
17 his6 ⊢B∈ℋ→B⋅ihB=0↔B=0ℎ
18 17 necon3bid ⊢B∈ℋ→B⋅ihB≠0↔B≠0ℎ
19 18 biimpar ⊢B∈ℋ∧B≠0ℎ→B⋅ihB≠0
20 19 adantr ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ→B⋅ihB≠0
21 13 16 20 divcan4d ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ→x⁢B⋅ihBB⋅ihB=x
22 21 adantr ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ∧A=x⋅ℎB→x⁢B⋅ihBB⋅ihB=x
23 12 22 eqtrd ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ∧A=x⋅ℎB→A⋅ihBnormℎ⁡B2=x
24 23 oveq1d ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ∧A=x⋅ℎB→A⋅ihBnormℎ⁡B2⋅ℎB=x⋅ℎB
25 simpr ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ∧A=x⋅ℎB→A=x⋅ℎB
26 24 25 eqtr4d ⊢B∈ℋ∧B≠0ℎ∧x∈ℂ∧A=x⋅ℎB→A⋅ihBnormℎ⁡B2⋅ℎB=A
27 26 rexlimdva2 ⊢B∈ℋ∧B≠0ℎ→∃x∈ℂA=x⋅ℎB→A⋅ihBnormℎ⁡B2⋅ℎB=A
28 2 27 sylbid ⊢B∈ℋ∧B≠0ℎ→A∈span⁡B→A⋅ihBnormℎ⁡B2⋅ℎB=A
29 28 3impia ⊢B∈ℋ∧B≠0ℎ∧A∈span⁡B→A⋅ihBnormℎ⁡B2⋅ℎB=A