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 ⊢ F = R freeLMod I
Assertion frlmsca ⊢ R ∈ V ∧ I ∈ W → R = Scalar ⁡ F

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢ F = R freeLMod I
2 fvex ⊢ ringLMod ⁡ R ∈ V
3 eqid ⊢ ringLMod ⁡ R ↑ 𝑠 I = ringLMod ⁡ R ↑ 𝑠 I
4 eqid ⊢ Scalar ⁡ ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R
5 3 4 pwssca ⊢ ringLMod ⁡ R ∈ V ∧ I ∈ W → Scalar ⁡ ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I
6 2 5 mpan ⊢ I ∈ W → Scalar ⁡ ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I
7 6 adantl ⊢ R ∈ V ∧ I ∈ W → Scalar ⁡ ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I
8 fvex ⊢ Base F ∈ V
9 eqid ⊢ ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F = ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
10 eqid ⊢ Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I
11 9 10 resssca ⊢ Base F ∈ V → Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
12 8 11 ax-mp ⊢ Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
13 7 12 eqtrdi ⊢ R ∈ V ∧ I ∈ W → Scalar ⁡ ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
14 rlmsca ⊢ R ∈ V → R = Scalar ⁡ ringLMod ⁡ R
15 14 adantr ⊢ R ∈ V ∧ I ∈ W → R = Scalar ⁡ ringLMod ⁡ R
16 eqid ⊢ Base F = Base F
17 1 16 frlmpws ⊢ R ∈ V ∧ I ∈ W → F = ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
18 17 fveq2d ⊢ R ∈ V ∧ I ∈ W → Scalar ⁡ F = Scalar ⁡ ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
19 13 15 18 3eqtr4d ⊢ R ∈ V ∧ I ∈ W → R = Scalar ⁡ F