Step |
Hyp |
Ref |
Expression |
1 |
|
frlmval.f |
⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 ) |
2 |
|
frlmbas.n |
⊢ 𝑁 = ( Base ‘ 𝑅 ) |
3 |
|
frlmbas.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
4 |
|
frlmbas.b |
⊢ 𝐵 = { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } |
5 |
|
fvex |
⊢ ( ringLMod ‘ 𝑅 ) ∈ V |
6 |
|
fnconstg |
⊢ ( ( ringLMod ‘ 𝑅 ) ∈ V → ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼 ) |
7 |
5 6
|
ax-mp |
⊢ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼 |
8 |
|
eqid |
⊢ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) |
9 |
|
eqid |
⊢ { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } = { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } |
10 |
8 9
|
dsmmbas2 |
⊢ ( ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } = ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) |
11 |
7 10
|
mpan |
⊢ ( 𝐼 ∈ 𝑊 → { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } = ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } = ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) |
13 |
|
fvco2 |
⊢ ( ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼 ∧ 𝑥 ∈ 𝐼 ) → ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) = ( 0g ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ) |
14 |
7 13
|
mpan |
⊢ ( 𝑥 ∈ 𝐼 → ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) = ( 0g ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ) |
15 |
14
|
adantl |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) = ( 0g ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ) |
16 |
5
|
fvconst2 |
⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( ringLMod ‘ 𝑅 ) ) |
17 |
16
|
adantl |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( ringLMod ‘ 𝑅 ) ) |
18 |
17
|
fveq2d |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 0g ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) ) |
19 |
|
rlm0 |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) |
20 |
3 19
|
eqtri |
⊢ 0 = ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) |
21 |
18 20
|
eqtr4di |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 0g ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = 0 ) |
22 |
15 21
|
eqtrd |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) = 0 ) |
23 |
22
|
neeq2d |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑘 ‘ 𝑥 ) ≠ ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) ↔ ( 𝑘 ‘ 𝑥 ) ≠ 0 ) ) |
24 |
23
|
rabbidva |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → { 𝑥 ∈ 𝐼 ∣ ( 𝑘 ‘ 𝑥 ) ≠ ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝐼 ∣ ( 𝑘 ‘ 𝑥 ) ≠ 0 } ) |
25 |
|
elmapfn |
⊢ ( 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) → 𝑘 Fn 𝐼 ) |
26 |
25
|
adantl |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝑘 Fn 𝐼 ) |
27 |
|
fn0g |
⊢ 0g Fn V |
28 |
|
ssv |
⊢ ran ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ⊆ V |
29 |
|
fnco |
⊢ ( ( 0g Fn V ∧ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼 ∧ ran ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ⊆ V ) → ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) Fn 𝐼 ) |
30 |
27 7 28 29
|
mp3an |
⊢ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) Fn 𝐼 |
31 |
|
fndmdif |
⊢ ( ( 𝑘 Fn 𝐼 ∧ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) Fn 𝐼 ) → dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑘 ‘ 𝑥 ) ≠ ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) } ) |
32 |
26 30 31
|
sylancl |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑘 ‘ 𝑥 ) ≠ ( ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ‘ 𝑥 ) } ) |
33 |
|
simplr |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝐼 ∈ 𝑊 ) |
34 |
3
|
fvexi |
⊢ 0 ∈ V |
35 |
34
|
a1i |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → 0 ∈ V ) |
36 |
|
suppvalfn |
⊢ ( ( 𝑘 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ∧ 0 ∈ V ) → ( 𝑘 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑘 ‘ 𝑥 ) ≠ 0 } ) |
37 |
26 33 35 36
|
syl3anc |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → ( 𝑘 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑘 ‘ 𝑥 ) ≠ 0 } ) |
38 |
24 32 37
|
3eqtr4d |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( 𝑘 supp 0 ) ) |
39 |
38
|
eleq1d |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → ( dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin ↔ ( 𝑘 supp 0 ) ∈ Fin ) ) |
40 |
|
elmapfun |
⊢ ( 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) → Fun 𝑘 ) |
41 |
|
id |
⊢ ( 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) → 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) |
42 |
34
|
a1i |
⊢ ( 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) → 0 ∈ V ) |
43 |
40 41 42
|
3jca |
⊢ ( 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) → ( Fun 𝑘 ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∧ 0 ∈ V ) ) |
44 |
43
|
adantl |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → ( Fun 𝑘 ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∧ 0 ∈ V ) ) |
45 |
|
funisfsupp |
⊢ ( ( Fun 𝑘 ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∧ 0 ∈ V ) → ( 𝑘 finSupp 0 ↔ ( 𝑘 supp 0 ) ∈ Fin ) ) |
46 |
44 45
|
syl |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → ( 𝑘 finSupp 0 ↔ ( 𝑘 supp 0 ) ∈ Fin ) ) |
47 |
39 46
|
bitr4d |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ) → ( dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin ↔ 𝑘 finSupp 0 ) ) |
48 |
47
|
rabbidva |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } = { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } ) |
49 |
|
eqid |
⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) |
50 |
|
rlmbas |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) |
51 |
2 50
|
eqtri |
⊢ 𝑁 = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) |
52 |
49 51
|
pwsbas |
⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
53 |
5 52
|
mpan |
⊢ ( 𝐼 ∈ 𝑊 → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
54 |
53
|
adantl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) |
55 |
|
eqid |
⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) |
56 |
49 55
|
pwsval |
⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
57 |
5 56
|
mpan |
⊢ ( 𝐼 ∈ 𝑊 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
58 |
57
|
adantl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
59 |
|
rlmsca |
⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) |
60 |
59
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) |
61 |
60
|
oveq1d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
62 |
58 61
|
eqtr4d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
63 |
62
|
fveq2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) |
64 |
54 63
|
eqtrd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) |
65 |
64
|
rabeqdv |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } = { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } ) |
66 |
48 65
|
eqtr3d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } = { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } ) |
67 |
4 66
|
syl5eq |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 = { 𝑘 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∣ dom ( 𝑘 ∖ ( 0g ∘ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ∈ Fin } ) |
68 |
1
|
frlmval |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) |
69 |
68
|
fveq2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) |
70 |
12 67 69
|
3eqtr4d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 = ( Base ‘ 𝐹 ) ) |