Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . 5
⊢
(ringLMod‘𝑅)
∈ V |
2 | | fnconstg 6006 |
. . . . 5
⊢
((ringLMod‘𝑅)
∈ V → (𝐼 ×
{(ringLMod‘𝑅)}) Fn
𝐼) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ (𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 |
4 | | eqid 2610 |
. . . . 5
⊢ (𝑅Xs(𝐼 × {(ringLMod‘𝑅)})) = (𝑅Xs(𝐼 × {(ringLMod‘𝑅)})) |
5 | | eqid 2610 |
. . . . 5
⊢ {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} = {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin} |
6 | 4, 5 | dsmmbas2 19900 |
. . . 4
⊢ (((𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} =
(Base‘(𝑅
⊕m (𝐼
× {(ringLMod‘𝑅)})))) |
7 | 3, 6 | mpan 702 |
. . 3
⊢ (𝐼 ∈ 𝑊 → {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} =
(Base‘(𝑅
⊕m (𝐼
× {(ringLMod‘𝑅)})))) |
8 | 7 | adantl 481 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} =
(Base‘(𝑅
⊕m (𝐼
× {(ringLMod‘𝑅)})))) |
9 | | frlmbas.b |
. . 3
⊢ 𝐵 = {𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∣ 𝑘 finSupp 0 } |
10 | | fvco2 6183 |
. . . . . . . . . . . . 13
⊢ (((𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥))) |
11 | 3, 10 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐼 → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥))) |
12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥))) |
13 | 1 | fvconst2 6374 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐼 → ((𝐼 × {(ringLMod‘𝑅)})‘𝑥) = (ringLMod‘𝑅)) |
14 | 13 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {(ringLMod‘𝑅)})‘𝑥) = (ringLMod‘𝑅)) |
15 | 14 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) ∧ 𝑥 ∈ 𝐼) → (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥)) =
(0g‘(ringLMod‘𝑅))) |
16 | | frlmbas.z |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝑅) |
17 | | rlm0 19018 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) =
(0g‘(ringLMod‘𝑅)) |
18 | 16, 17 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘(ringLMod‘𝑅)) |
19 | 15, 18 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) ∧ 𝑥 ∈ 𝐼) → (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥)) = 0 ) |
20 | 12, 19 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = 0 ) |
21 | 20 | neeq2d 2842 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) ↔ (𝑘‘𝑥) ≠ 0 )) |
22 | 21 | rabbidva 3163 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥)} = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ 0 }) |
23 | | elmapfn 7766 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑁 ↑𝑚 𝐼) → 𝑘 Fn 𝐼) |
24 | 23 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → 𝑘 Fn 𝐼) |
25 | | fn0g 17085 |
. . . . . . . . . 10
⊢
0g Fn V |
26 | | ssv 3588 |
. . . . . . . . . 10
⊢ ran
(𝐼 ×
{(ringLMod‘𝑅)})
⊆ V |
27 | | fnco 5913 |
. . . . . . . . . 10
⊢
((0g Fn V ∧ (𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 ∧ ran (𝐼 × {(ringLMod‘𝑅)}) ⊆ V) → (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)})) Fn
𝐼) |
28 | 25, 3, 26, 27 | mp3an 1416 |
. . . . . . . . 9
⊢
(0g ∘ (𝐼 × {(ringLMod‘𝑅)})) Fn 𝐼 |
29 | | fndmdif 6229 |
. . . . . . . . 9
⊢ ((𝑘 Fn 𝐼 ∧ (0g ∘ (𝐼 × {(ringLMod‘𝑅)})) Fn 𝐼) → dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥)}) |
30 | 24, 28, 29 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → dom (𝑘 ∖ (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)}))) =
{𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥)}) |
31 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → 𝐼 ∈ 𝑊) |
32 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V |
33 | 16, 32 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 0 ∈
V |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → 0 ∈ V) |
35 | | suppvalfn 7189 |
. . . . . . . . 9
⊢ ((𝑘 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ∧ 0 ∈ V) → (𝑘 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ 0 }) |
36 | 24, 31, 34, 35 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → (𝑘 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ 0 }) |
37 | 22, 30, 36 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → dom (𝑘 ∖ (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)}))) =
(𝑘 supp 0 )) |
38 | 37 | eleq1d 2672 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → (dom (𝑘 ∖ (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)})))
∈ Fin ↔ (𝑘 supp
0 )
∈ Fin)) |
39 | | elmapfun 7767 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑁 ↑𝑚 𝐼) → Fun 𝑘) |
40 | | id 22 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑁 ↑𝑚 𝐼) → 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) |
41 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑁 ↑𝑚 𝐼) → 0 ∈ V) |
42 | 39, 40, 41 | 3jca 1235 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑁 ↑𝑚 𝐼) → (Fun 𝑘 ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∧ 0 ∈
V)) |
43 | 42 | adantl 481 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → (Fun 𝑘 ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∧ 0 ∈
V)) |
44 | | funisfsupp 8163 |
. . . . . . 7
⊢ ((Fun
𝑘 ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∧ 0 ∈ V) → (𝑘 finSupp 0 ↔ (𝑘 supp 0 ) ∈
Fin)) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → (𝑘 finSupp 0 ↔ (𝑘 supp 0 ) ∈
Fin)) |
46 | 38, 45 | bitr4d 270 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑𝑚 𝐼)) → (dom (𝑘 ∖ (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)})))
∈ Fin ↔ 𝑘 finSupp
0
)) |
47 | 46 | rabbidva 3163 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∣ dom (𝑘 ∖ (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)})))
∈ Fin} = {𝑘 ∈
(𝑁
↑𝑚 𝐼) ∣ 𝑘 finSupp 0 }) |
48 | | eqid 2610 |
. . . . . . . . 9
⊢
((ringLMod‘𝑅)
↑s 𝐼) = ((ringLMod‘𝑅) ↑s 𝐼) |
49 | | frlmbas.n |
. . . . . . . . . 10
⊢ 𝑁 = (Base‘𝑅) |
50 | | rlmbas 19016 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) |
51 | 49, 50 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝑁 =
(Base‘(ringLMod‘𝑅)) |
52 | 48, 51 | pwsbas 15970 |
. . . . . . . 8
⊢
(((ringLMod‘𝑅)
∈ V ∧ 𝐼 ∈
𝑊) → (𝑁 ↑𝑚
𝐼) =
(Base‘((ringLMod‘𝑅) ↑s 𝐼))) |
53 | 1, 52 | mpan 702 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑊 → (𝑁 ↑𝑚 𝐼) =
(Base‘((ringLMod‘𝑅) ↑s 𝐼))) |
54 | 53 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑁 ↑𝑚 𝐼) =
(Base‘((ringLMod‘𝑅) ↑s 𝐼))) |
55 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Scalar‘(ringLMod‘𝑅)) = (Scalar‘(ringLMod‘𝑅)) |
56 | 48, 55 | pwsval 15969 |
. . . . . . . . . 10
⊢
(((ringLMod‘𝑅)
∈ V ∧ 𝐼 ∈
𝑊) →
((ringLMod‘𝑅)
↑s 𝐼) = ((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) |
57 | 1, 56 | mpan 702 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑊 → ((ringLMod‘𝑅) ↑s 𝐼) =
((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) |
58 | 57 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((ringLMod‘𝑅) ↑s 𝐼) =
((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) |
59 | | rlmsca 19021 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(ringLMod‘𝑅))) |
60 | 59 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑅 = (Scalar‘(ringLMod‘𝑅))) |
61 | 60 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑅Xs(𝐼 × {(ringLMod‘𝑅)})) = ((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) |
62 | 58, 61 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((ringLMod‘𝑅) ↑s 𝐼) = (𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) |
63 | 62 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘((ringLMod‘𝑅) ↑s
𝐼)) = (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)})))) |
64 | 54, 63 | eqtrd 2644 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑁 ↑𝑚 𝐼) = (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)})))) |
65 | | rabeq 3166 |
. . . . 5
⊢ ((𝑁 ↑𝑚
𝐼) = (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) → {𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∣ dom (𝑘 ∖ (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)})))
∈ Fin} = {𝑘 ∈
(Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin}) |
66 | 64, 65 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∣ dom (𝑘 ∖ (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)})))
∈ Fin} = {𝑘 ∈
(Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin}) |
67 | 47, 66 | eqtr3d 2646 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (𝑁 ↑𝑚 𝐼) ∣ 𝑘 finSupp 0 } = {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin}) |
68 | 9, 67 | syl5eq 2656 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin}) |
69 | | frlmval.f |
. . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
70 | 69 | frlmval 19911 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹 = (𝑅 ⊕m (𝐼 × {(ringLMod‘𝑅)}))) |
71 | 70 | fveq2d 6107 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝐹) = (Base‘(𝑅 ⊕m (𝐼 × {(ringLMod‘𝑅)})))) |
72 | 8, 68, 71 | 3eqtr4d 2654 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = (Base‘𝐹)) |