Metamath Proof Explorer

Theorem frlmpws

Description: The free module as a restriction of the power module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses frlmval.f ⊢ F = R freeLMod I
frlmpws.b ⊢ B = Base F
Assertion frlmpws ⊢ R ∈ V ∧ I ∈ W → F = ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 B

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢ F = R freeLMod I
2 frlmpws.b ⊢ B = Base F
3 eqid ⊢ Base R ⊕ m I × ringLMod ⁡ R = Base R ⊕ m I × ringLMod ⁡ R
4 3 dsmmval2 ⊢ R ⊕ m I × ringLMod ⁡ R = R ⨉ 𝑠 I × ringLMod ⁡ R ↾ 𝑠 Base R ⊕ m I × ringLMod ⁡ R
5 rlmsca ⊢ R ∈ V → R = Scalar ⁡ ringLMod ⁡ R
6 5 adantr ⊢ R ∈ V ∧ I ∈ W → R = Scalar ⁡ ringLMod ⁡ R
7 6 oveq1d ⊢ R ∈ V ∧ I ∈ W → R ⨉ 𝑠 I × ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R ⨉ 𝑠 I × ringLMod ⁡ R
8 1 frlmval ⊢ R ∈ V ∧ I ∈ W → F = R ⊕ m I × ringLMod ⁡ R
9 8 eqcomd ⊢ R ∈ V ∧ I ∈ W → R ⊕ m I × ringLMod ⁡ R = F
10 9 fveq2d ⊢ R ∈ V ∧ I ∈ W → Base R ⊕ m I × ringLMod ⁡ R = Base F
11 10 2 eqtr4di ⊢ R ∈ V ∧ I ∈ W → Base R ⊕ m I × ringLMod ⁡ R = B
12 7 11 oveq12d ⊢ R ∈ V ∧ I ∈ W → R ⨉ 𝑠 I × ringLMod ⁡ R ↾ 𝑠 Base R ⊕ m I × ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R ⨉ 𝑠 I × ringLMod ⁡ R ↾ 𝑠 B
13 4 12 syl5eq ⊢ R ∈ V ∧ I ∈ W → R ⊕ m I × ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R ⨉ 𝑠 I × ringLMod ⁡ R ↾ 𝑠 B
14 fvex ⊢ ringLMod ⁡ R ∈ V
15 eqid ⊢ ringLMod ⁡ R ↑ 𝑠 I = ringLMod ⁡ R ↑ 𝑠 I
16 eqid ⊢ Scalar ⁡ ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R
17 15 16 pwsval ⊢ ringLMod ⁡ R ∈ V ∧ I ∈ W → ringLMod ⁡ R ↑ 𝑠 I = Scalar ⁡ ringLMod ⁡ R ⨉ 𝑠 I × ringLMod ⁡ R
18 14 17 mpan ⊢ I ∈ W → ringLMod ⁡ R ↑ 𝑠 I = Scalar ⁡ ringLMod ⁡ R ⨉ 𝑠 I × ringLMod ⁡ R
19 18 adantl ⊢ R ∈ V ∧ I ∈ W → ringLMod ⁡ R ↑ 𝑠 I = Scalar ⁡ ringLMod ⁡ R ⨉ 𝑠 I × ringLMod ⁡ R
20 19 oveq1d ⊢ R ∈ V ∧ I ∈ W → ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 B = Scalar ⁡ ringLMod ⁡ R ⨉ 𝑠 I × ringLMod ⁡ R ↾ 𝑠 B
21 13 8 20 3eqtr4d ⊢ R ∈ V ∧ I ∈ W → F = ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 B