Metamath Proof Explorer

Theorem lnopmul

Description: Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopmul ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→T⁡A⋅ℎB=A⋅ℎT⁡B

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢0ℎ∈ℋ
2 lnopl ⊢T∈LinOp∧A∈ℂ∧B∈ℋ∧0ℎ∈ℋ→T⁡A⋅ℎB+ℎ0ℎ=A⋅ℎT⁡B+ℎT⁡0ℎ
3 1 2 mpanr2 ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→T⁡A⋅ℎB+ℎ0ℎ=A⋅ℎT⁡B+ℎT⁡0ℎ
4 3 3impa ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→T⁡A⋅ℎB+ℎ0ℎ=A⋅ℎT⁡B+ℎT⁡0ℎ
5 hvmulcl ⊢A∈ℂ∧B∈ℋ→A⋅ℎB∈ℋ
6 ax-hvaddid ⊢A⋅ℎB∈ℋ→A⋅ℎB+ℎ0ℎ=A⋅ℎB
7 5 6 syl ⊢A∈ℂ∧B∈ℋ→A⋅ℎB+ℎ0ℎ=A⋅ℎB
8 7 3adant1 ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→A⋅ℎB+ℎ0ℎ=A⋅ℎB
9 8 fveq2d ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→T⁡A⋅ℎB+ℎ0ℎ=T⁡A⋅ℎB
10 lnop0 ⊢T∈LinOp→T⁡0ℎ=0ℎ
11 10 oveq2d ⊢T∈LinOp→A⋅ℎT⁡B+ℎT⁡0ℎ=A⋅ℎT⁡B+ℎ0ℎ
12 11 3ad2ant1 ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→A⋅ℎT⁡B+ℎT⁡0ℎ=A⋅ℎT⁡B+ℎ0ℎ
13 lnopf ⊢T∈LinOp→T:ℋ⟶ℋ
14 13 ffvelcdmda ⊢T∈LinOp∧B∈ℋ→T⁡B∈ℋ
15 hvmulcl ⊢A∈ℂ∧T⁡B∈ℋ→A⋅ℎT⁡B∈ℋ
16 14 15 sylan2 ⊢A∈ℂ∧T∈LinOp∧B∈ℋ→A⋅ℎT⁡B∈ℋ
17 16 3impb ⊢A∈ℂ∧T∈LinOp∧B∈ℋ→A⋅ℎT⁡B∈ℋ
18 17 3com12 ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→A⋅ℎT⁡B∈ℋ
19 ax-hvaddid ⊢A⋅ℎT⁡B∈ℋ→A⋅ℎT⁡B+ℎ0ℎ=A⋅ℎT⁡B
20 18 19 syl ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→A⋅ℎT⁡B+ℎ0ℎ=A⋅ℎT⁡B
21 12 20 eqtrd ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→A⋅ℎT⁡B+ℎT⁡0ℎ=A⋅ℎT⁡B
22 4 9 21 3eqtr3d ⊢T∈LinOp∧A∈ℂ∧B∈ℋ→T⁡A⋅ℎB=A⋅ℎT⁡B