Step |
Hyp |
Ref |
Expression |
1 |
|
frlmval.f |
⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 ) |
2 |
|
frlmpws.b |
⊢ 𝐵 = ( Base ‘ 𝐹 ) |
3 |
|
eqid |
⊢ ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
4 |
3
|
dsmmval2 |
⊢ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) |
5 |
|
rlmsca |
⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) |
6 |
5
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) |
7 |
6
|
oveq1d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
8 |
1
|
frlmval |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
9 |
8
|
eqcomd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = 𝐹 ) |
10 |
9
|
fveq2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( Base ‘ 𝐹 ) ) |
11 |
10 2
|
eqtr4di |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = 𝐵 ) |
12 |
7 11
|
oveq12d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) = ( ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s 𝐵 ) ) |
13 |
4 12
|
syl5eq |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s 𝐵 ) ) |
14 |
|
fvex |
⊢ ( ringLMod ‘ 𝑅 ) ∈ V |
15 |
|
eqid |
⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) |
16 |
|
eqid |
⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) |
17 |
15 16
|
pwsval |
⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
18 |
14 17
|
mpan |
⊢ ( 𝐼 ∈ 𝑊 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
19 |
18
|
adantl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
20 |
19
|
oveq1d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) = ( ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s 𝐵 ) ) |
21 |
13 8 20
|
3eqtr4d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) |