This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐹 ) )