Step |
Hyp |
Ref |
Expression |
1 |
|
frlmval.f |
⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 ) |
2 |
|
frlm0.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
3 |
|
rlmlmod |
⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod ) |
4 |
|
eqid |
⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) |
5 |
4
|
pwslmod |
⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod ) |
6 |
3 5
|
sylan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 ) |
8 |
|
eqid |
⊢ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) |
9 |
1 7 8
|
frlmlss |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝐹 ) ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
10 |
8
|
lsssubg |
⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod ∧ ( Base ‘ 𝐹 ) ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) → ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
11 |
6 9 10
|
syl2anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
12 |
|
eqid |
⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) |
13 |
|
eqid |
⊢ ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) |
14 |
12 13
|
subg0 |
⊢ ( ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) ) |
15 |
11 14
|
syl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) ) |
16 |
|
lmodgrp |
⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → ( ringLMod ‘ 𝑅 ) ∈ Grp ) |
17 |
|
grpmnd |
⊢ ( ( ringLMod ‘ 𝑅 ) ∈ Grp → ( ringLMod ‘ 𝑅 ) ∈ Mnd ) |
18 |
3 16 17
|
3syl |
⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ Mnd ) |
19 |
|
rlm0 |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) |
20 |
2 19
|
eqtri |
⊢ 0 = ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) |
21 |
4 20
|
pws0g |
⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
22 |
18 21
|
sylan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
23 |
1 7
|
frlmpws |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) |
24 |
23
|
fveq2d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( 0g ‘ 𝐹 ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) ) |
25 |
15 22 24
|
3eqtr4d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ 𝐹 ) ) |