Theorem clmcj

Description: The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypothesis	clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	clmcj	⊢ ( 𝑊 ∈ ℂMod → ∗ = ( *𝑟 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		fvex	⊢ ( Base ‘ 𝐹 ) ∈ V
3		eqid	⊢ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) = ( ℂfld ↾s ( Base ‘ 𝐹 ) )
4		cnfldcj	⊢ ∗ = ( *𝑟 ‘ ℂfld )
5	3 4	ressstarv	⊢ ( ( Base ‘ 𝐹 ) ∈ V → ∗ = ( *𝑟 ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
6	2 5	ax-mp	⊢ ∗ = ( *𝑟 ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
7		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
8	1 7	clmsca	⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
9	8	fveq2d	⊢ ( 𝑊 ∈ ℂMod → ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
10	6 9	eqtr4id	⊢ ( 𝑊 ∈ ℂMod → ∗ = ( *𝑟 ‘ 𝐹 ) )