Theorem homco2

Description: Move a scalar product out of a composition of operators. The operator T must be linear, unlike homco1 that works for any operators. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	homco2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) = ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝐴 ∈ ℂ )
2		simpl3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝑈 : ℋ ⟶ ℋ )
3		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
4		homval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ·op 𝑈 ) ‘ 𝑥 ) = ( 𝐴 ·ℎ ( 𝑈 ‘ 𝑥 ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ·op 𝑈 ) ‘ 𝑥 ) = ( 𝐴 ·ℎ ( 𝑈 ‘ 𝑥 ) ) )
6	5	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐴 ·op 𝑈 ) ‘ 𝑥 ) ) = ( 𝑇 ‘ ( 𝐴 ·ℎ ( 𝑈 ‘ 𝑥 ) ) ) )
7		homulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑈 ) : ℋ ⟶ ℋ )
8	7	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑈 ) : ℋ ⟶ ℋ )
9		fvco3	⊢ ( ( ( 𝐴 ·op 𝑈 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) ‘ 𝑥 ) = ( 𝑇 ‘ ( ( 𝐴 ·op 𝑈 ) ‘ 𝑥 ) ) )
10	8 9	sylan	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) ‘ 𝑥 ) = ( 𝑇 ‘ ( ( 𝐴 ·op 𝑈 ) ‘ 𝑥 ) ) )
11		fvco3	⊢ ( ( 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑈 ‘ 𝑥 ) ) )
12	2 3 11	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑈 ‘ 𝑥 ) ) )
13	12	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝐴 ·ℎ ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ ( 𝑈 ‘ 𝑥 ) ) ) )
14		lnopf	⊢ ( 𝑇 ∈ LinOp → 𝑇 : ℋ ⟶ ℋ )
15	14	3ad2ant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → 𝑇 : ℋ ⟶ ℋ )
16		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → 𝑈 : ℋ ⟶ ℋ )
17		fco	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ )
18	15 16 17	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ )
19	18	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ )
20		homval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ‘ 𝑥 ) = ( 𝐴 ·ℎ ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ) )
21	1 19 3 20	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ‘ 𝑥 ) = ( 𝐴 ·ℎ ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ) )
22		simpl2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝑇 ∈ LinOp )
23	16	ffvelrnda	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑈 ‘ 𝑥 ) ∈ ℋ )
24		lnopmul	⊢ ( ( 𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ ∧ ( 𝑈 ‘ 𝑥 ) ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ ( 𝑈 ‘ 𝑥 ) ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ ( 𝑈 ‘ 𝑥 ) ) ) )
25	22 1 23 24	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ ( 𝑈 ‘ 𝑥 ) ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ ( 𝑈 ‘ 𝑥 ) ) ) )
26	13 21 25	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝐴 ·ℎ ( 𝑈 ‘ 𝑥 ) ) ) )
27	6 10 26	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) ‘ 𝑥 ) = ( ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ‘ 𝑥 ) )
28	27	ralrimiva	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ∀ 𝑥 ∈ ℋ ( ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) ‘ 𝑥 ) = ( ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ‘ 𝑥 ) )
29		fco	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝐴 ·op 𝑈 ) : ℋ ⟶ ℋ ) → ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) : ℋ ⟶ ℋ )
30	15 8 29	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) : ℋ ⟶ ℋ )
31		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → 𝐴 ∈ ℂ )
32		homulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ ) → ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) : ℋ ⟶ ℋ )
33	31 18 32	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) : ℋ ⟶ ℋ )
34		hoeq	⊢ ( ( ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) : ℋ ⟶ ℋ ∧ ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) ‘ 𝑥 ) = ( ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ‘ 𝑥 ) ↔ ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) = ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ) )
35	30 33 34	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) ‘ 𝑥 ) = ( ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ‘ 𝑥 ) ↔ ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) = ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) ) )
36	28 35	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 ∘ ( 𝐴 ·op 𝑈 ) ) = ( 𝐴 ·op ( 𝑇 ∘ 𝑈 ) ) )