# Metamath Proof Explorer

## Theorem eigvec1

Description: Property of an eigenvector. (Contributed by NM, 12-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigvec1 ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left({T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)$

### Proof

Step Hyp Ref Expression
1 eigvalval ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \mathrm{eigval}\left({T}\right)\left({A}\right)=\frac{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}}{{{norm}_{ℎ}\left({A}\right)}^{2}}$
2 1 oveq1d ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}=\left(\frac{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}}{{{norm}_{ℎ}\left({A}\right)}^{2}}\right){\cdot }_{ℎ}{A}$
3 eleigvec2 ${⊢}{T}:ℋ⟶ℋ\to \left({A}\in \mathrm{eigvec}\left({T}\right)↔\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)\right)$
4 3 biimpa ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)$
5 normcan ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\wedge {T}\left({A}\right)\in \mathrm{span}\left(\left\{{A}\right\}\right)\right)\to \left(\frac{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}}{{{norm}_{ℎ}\left({A}\right)}^{2}}\right){\cdot }_{ℎ}{A}={T}\left({A}\right)$
6 4 5 syl ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left(\frac{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}}{{{norm}_{ℎ}\left({A}\right)}^{2}}\right){\cdot }_{ℎ}{A}={T}\left({A}\right)$
7 2 6 eqtr2d ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to {T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}$
8 4 simp2d ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to {A}\ne {0}_{ℎ}$
9 7 8 jca ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left({T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)$