Theorem frlmsca

Description: The ring of scalars of a free module. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypothesis	frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
Assertion	frlmsca	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		fvex	⊢ ( ringLMod ‘ 𝑅 ) ∈ V
3		eqid	⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
4		eqid	⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
5	3 4	pwssca	⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
6	2 5	mpan	⊢ ( 𝐼 ∈ 𝑊 → ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
7	6	adantl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
8		fvex	⊢ ( Base ‘ 𝐹 ) ∈ V
9		eqid	⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) )
10		eqid	⊢ ( Scalar ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Scalar ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
11	9 10	resssca	⊢ ( ( Base ‘ 𝐹 ) ∈ V → ( Scalar ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Scalar ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) )
12	8 11	ax-mp	⊢ ( Scalar ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Scalar ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) )
13	7 12	eqtrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) )
14		rlmsca	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
15	14	adantr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
16		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
17	1 16	frlmpws	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) )
18	17	fveq2d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝐹 ) = ( Scalar ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) )
19	13 15 18	3eqtr4d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )