# Metamath Proof Explorer

## Theorem eigorth

Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigorth ${⊢}\left(\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\wedge \left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
2 oveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {C}{\cdot }_{ℎ}{A}={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
3 1 2 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}↔{T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
4 3 anbi1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)↔\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\right)$
5 4 anbi1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)↔\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\right)$
6 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)$
7 1 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}$
8 6 7 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}\right)$
9 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}$
10 9 eqeq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{B}=0↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=0\right)$
11 8 10 bibi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=0\right)\right)$
12 5 11 imbi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left(\left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)\right)↔\left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=0\right)\right)\right)$
13 fveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left({B}\right)={T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
14 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {D}{\cdot }_{ℎ}{B}={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
15 13 14 eqeq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({T}\left({B}\right)={D}{\cdot }_{ℎ}{B}↔{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
16 15 anbi2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)↔\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
17 16 anbi1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)↔\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\right)$
18 13 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
19 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
20 18 19 eqeq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
21 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
22 21 eqeq1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=0↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)$
23 20 22 bibi12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=0\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)\right)$
24 17 23 imbi12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(\left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=0\right)\right)↔\left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)\right)\right)$
25 oveq1 ${⊢}{C}=if\left({C}\in ℂ,{C},0\right)\to {C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
26 25 eqeq2d ${⊢}{C}=if\left({C}\in ℂ,{C},0\right)\to \left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)↔{T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
27 26 anbi1d ${⊢}{C}=if\left({C}\in ℂ,{C},0\right)\to \left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)↔\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
28 neeq1 ${⊢}{C}=if\left({C}\in ℂ,{C},0\right)\to \left({C}\ne \stackrel{‾}{{D}}↔if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{{D}}\right)$
29 27 28 anbi12d ${⊢}{C}=if\left({C}\in ℂ,{C},0\right)\to \left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)↔\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{{D}}\right)\right)$
30 29 imbi1d ${⊢}{C}=if\left({C}\in ℂ,{C},0\right)\to \left(\left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)={C}{\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)\right)↔\left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{{D}}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)\right)\right)$
31 oveq1 ${⊢}{D}=if\left({D}\in ℂ,{D},0\right)\to {D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=if\left({D}\in ℂ,{D},0\right){\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
32 31 eqeq2d ${⊢}{D}=if\left({D}\in ℂ,{D},0\right)\to \left({T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)=if\left({D}\in ℂ,{D},0\right){\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
33 32 anbi2d ${⊢}{D}=if\left({D}\in ℂ,{D},0\right)\to \left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)↔\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)=if\left({D}\in ℂ,{D},0\right){\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
34 fveq2 ${⊢}{D}=if\left({D}\in ℂ,{D},0\right)\to \stackrel{‾}{{D}}=\stackrel{‾}{if\left({D}\in ℂ,{D},0\right)}$
35 34 neeq2d ${⊢}{D}=if\left({D}\in ℂ,{D},0\right)\to \left(if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{{D}}↔if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{if\left({D}\in ℂ,{D},0\right)}\right)$
36 33 35 anbi12d ${⊢}{D}=if\left({D}\in ℂ,{D},0\right)\to \left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{{D}}\right)↔\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)=if\left({D}\in ℂ,{D},0\right){\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{if\left({D}\in ℂ,{D},0\right)}\right)\right)$
37 36 imbi1d ${⊢}{D}=if\left({D}\in ℂ,{D},0\right)\to \left(\left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={D}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{{D}}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)\right)↔\left(\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)=if\left({D}\in ℂ,{D},0\right){\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{if\left({D}\in ℂ,{D},0\right)}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)\right)\right)$
38 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
39 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
40 0cn ${⊢}0\in ℂ$
41 40 elimel ${⊢}if\left({C}\in ℂ,{C},0\right)\in ℂ$
42 40 elimel ${⊢}if\left({D}\in ℂ,{D},0\right)\in ℂ$
43 38 39 41 42 eigorthi ${⊢}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({C}\in ℂ,{C},0\right){\cdot }_{ℎ}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\wedge {T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)=if\left({D}\in ℂ,{D},0\right){\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\wedge if\left({C}\in ℂ,{C},0\right)\ne \stackrel{‾}{if\left({D}\in ℂ,{D},0\right)}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{T}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=0\right)$
44 12 24 30 37 43 dedth4h ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to \left(\left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)\right)$
45 44 imp ${⊢}\left(\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\wedge \left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)$