| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvex 6918 | . . . . 5
⊢
(ringLMod‘𝑅)
∈ V | 
| 2 |  | fnconstg 6795 | . . . . 5
⊢
((ringLMod‘𝑅)
∈ V → (𝐼 ×
{(ringLMod‘𝑅)}) Fn
𝐼) | 
| 3 | 1, 2 | ax-mp 5 | . . . 4
⊢ (𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 | 
| 4 |  | eqid 2736 | . . . . 5
⊢ (𝑅Xs(𝐼 × {(ringLMod‘𝑅)})) = (𝑅Xs(𝐼 × {(ringLMod‘𝑅)})) | 
| 5 |  | eqid 2736 | . . . . 5
⊢ {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} = {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin} | 
| 6 | 4, 5 | dsmmbas2 21758 | . . . 4
⊢ (((𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} =
(Base‘(𝑅
⊕m (𝐼
× {(ringLMod‘𝑅)})))) | 
| 7 | 3, 6 | mpan 690 | . . 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
⊢ 𝐵 = {𝑘 ∈ (𝑁 ↑m 𝐼) ∣ 𝑘 finSupp 0 } | 
| 10 |  | fvco2 7005 | . . . . . . . . . . . . 13
⊢ (((𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥))) | 
| 11 | 3, 10 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐼 → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥))) | 
| 12 | 11 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥))) | 
| 13 | 1 | fvconst2 7225 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐼 → ((𝐼 × {(ringLMod‘𝑅)})‘𝑥) = (ringLMod‘𝑅)) | 
| 14 | 13 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {(ringLMod‘𝑅)})‘𝑥) = (ringLMod‘𝑅)) | 
| 15 | 14 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥)) =
(0g‘(ringLMod‘𝑅))) | 
| 16 |  | frlmbas.z | . . . . . . . . . . . . 13
⊢  0 =
(0g‘𝑅) | 
| 17 |  | rlm0 21203 | . . . . . . . . . . . . 13
⊢
(0g‘𝑅) =
(0g‘(ringLMod‘𝑅)) | 
| 18 | 16, 17 | eqtri 2764 | . . . . . . . . . . . 12
⊢  0 =
(0g‘(ringLMod‘𝑅)) | 
| 19 | 15, 18 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → (0g‘((𝐼 × {(ringLMod‘𝑅)})‘𝑥)) = 0 ) | 
| 20 | 12, 19 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) = 0 ) | 
| 21 | 20 | neeq2d 3000 | . . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥) ↔ (𝑘‘𝑥) ≠ 0 )) | 
| 22 | 21 | rabbidva 3442 | . . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥)} = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ 0 }) | 
| 23 |  | elmapfn 8906 | . . . . . . . . . 10
⊢ (𝑘 ∈ (𝑁 ↑m 𝐼) → 𝑘 Fn 𝐼) | 
| 24 | 23 | adantl 481 | . . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → 𝑘 Fn 𝐼) | 
| 25 |  | fn0g 18677 | . . . . . . . . . 10
⊢
0g Fn V | 
| 26 |  | ssv 4007 | . . . . . . . . . 10
⊢ ran
(𝐼 ×
{(ringLMod‘𝑅)})
⊆ V | 
| 27 |  | fnco 6685 | . . . . . . . . . 10
⊢
((0g Fn V ∧ (𝐼 × {(ringLMod‘𝑅)}) Fn 𝐼 ∧ ran (𝐼 × {(ringLMod‘𝑅)}) ⊆ V) → (0g ∘
(𝐼 ×
{(ringLMod‘𝑅)})) Fn
𝐼) | 
| 28 | 25, 3, 26, 27 | mp3an 1462 | . . . . . . . . 9
⊢
(0g ∘ (𝐼 × {(ringLMod‘𝑅)})) Fn 𝐼 | 
| 29 |  | fndmdif 7061 | . . . . . . . . 9
⊢ ((𝑘 Fn 𝐼 ∧ (0g ∘ (𝐼 × {(ringLMod‘𝑅)})) Fn 𝐼) → dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥)}) | 
| 30 | 24, 28, 29 | sylancl 586 | . . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ ((0g ∘ (𝐼 × {(ringLMod‘𝑅)}))‘𝑥)}) | 
| 31 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → 𝐼 ∈ 𝑊) | 
| 32 | 16 | fvexi 6919 | . . . . . . . . . 10
⊢  0 ∈
V | 
| 33 | 32 | a1i 11 | . . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → 0 ∈ V) | 
| 34 |  | suppvalfn 8194 | . . . . . . . . 9
⊢ ((𝑘 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ∧ 0 ∈ V) → (𝑘 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ 0 }) | 
| 35 | 24, 31, 33, 34 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → (𝑘 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑘‘𝑥) ≠ 0 }) | 
| 36 | 22, 30, 35 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) = (𝑘 supp 0 )) | 
| 37 | 36 | eleq1d 2825 | . . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → (dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin ↔ (𝑘 supp 0 ) ∈
Fin)) | 
| 38 |  | elmapfun 8907 | . . . . . . . . 9
⊢ (𝑘 ∈ (𝑁 ↑m 𝐼) → Fun 𝑘) | 
| 39 |  | id 22 | . . . . . . . . 9
⊢ (𝑘 ∈ (𝑁 ↑m 𝐼) → 𝑘 ∈ (𝑁 ↑m 𝐼)) | 
| 40 | 32 | a1i 11 | . . . . . . . . 9
⊢ (𝑘 ∈ (𝑁 ↑m 𝐼) → 0 ∈ V) | 
| 41 | 38, 39, 40 | 3jca 1128 | . . . . . . . 8
⊢ (𝑘 ∈ (𝑁 ↑m 𝐼) → (Fun 𝑘 ∧ 𝑘 ∈ (𝑁 ↑m 𝐼) ∧ 0 ∈
V)) | 
| 42 | 41 | adantl 481 | . . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → (Fun 𝑘 ∧ 𝑘 ∈ (𝑁 ↑m 𝐼) ∧ 0 ∈
V)) | 
| 43 |  | funisfsupp 9408 | . . . . . . 7
⊢ ((Fun
𝑘 ∧ 𝑘 ∈ (𝑁 ↑m 𝐼) ∧ 0 ∈ V) → (𝑘 finSupp 0 ↔ (𝑘 supp 0 ) ∈
Fin)) | 
| 44 | 42, 43 | syl 17 | . . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → (𝑘 finSupp 0 ↔ (𝑘 supp 0 ) ∈
Fin)) | 
| 45 | 37, 44 | bitr4d 282 | . . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝑘 ∈ (𝑁 ↑m 𝐼)) → (dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin ↔ 𝑘 finSupp 0 )) | 
| 46 | 45 | rabbidva 3442 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (𝑁 ↑m 𝐼) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} = {𝑘 ∈ (𝑁 ↑m 𝐼) ∣ 𝑘 finSupp 0 }) | 
| 47 |  | eqid 2736 | . . . . . . . . 9
⊢
((ringLMod‘𝑅)
↑s 𝐼) = ((ringLMod‘𝑅) ↑s 𝐼) | 
| 48 |  | frlmbas.n | . . . . . . . . . 10
⊢ 𝑁 = (Base‘𝑅) | 
| 49 |  | rlmbas 21201 | . . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) | 
| 50 | 48, 49 | eqtri 2764 | . . . . . . . . 9
⊢ 𝑁 =
(Base‘(ringLMod‘𝑅)) | 
| 51 | 47, 50 | pwsbas 17533 | . . . . . . . 8
⊢
(((ringLMod‘𝑅)
∈ V ∧ 𝐼 ∈
𝑊) → (𝑁 ↑m 𝐼) =
(Base‘((ringLMod‘𝑅) ↑s 𝐼))) | 
| 52 | 1, 51 | mpan 690 | . . . . . . 7
⊢ (𝐼 ∈ 𝑊 → (𝑁 ↑m 𝐼) = (Base‘((ringLMod‘𝑅) ↑s
𝐼))) | 
| 53 | 52 | adantl 481 | . . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑁 ↑m 𝐼) = (Base‘((ringLMod‘𝑅) ↑s
𝐼))) | 
| 54 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Scalar‘(ringLMod‘𝑅)) = (Scalar‘(ringLMod‘𝑅)) | 
| 55 | 47, 54 | pwsval 17532 | . . . . . . . . . 10
⊢
(((ringLMod‘𝑅)
∈ V ∧ 𝐼 ∈
𝑊) →
((ringLMod‘𝑅)
↑s 𝐼) = ((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) | 
| 56 | 1, 55 | mpan 690 | . . . . . . . . 9
⊢ (𝐼 ∈ 𝑊 → ((ringLMod‘𝑅) ↑s 𝐼) =
((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) | 
| 57 | 56 | adantl 481 | . . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((ringLMod‘𝑅) ↑s 𝐼) =
((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) | 
| 58 |  | rlmsca 21206 | . . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(ringLMod‘𝑅))) | 
| 59 | 58 | adantr 480 | . . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑅 = (Scalar‘(ringLMod‘𝑅))) | 
| 60 | 59 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑅Xs(𝐼 × {(ringLMod‘𝑅)})) = ((Scalar‘(ringLMod‘𝑅))Xs(𝐼 × {(ringLMod‘𝑅)}))) | 
| 61 | 57, 60 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((ringLMod‘𝑅) ↑s 𝐼) = (𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) | 
| 62 | 61 | fveq2d 6909 | . . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘((ringLMod‘𝑅) ↑s
𝐼)) = (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)})))) | 
| 63 | 53, 62 | eqtrd 2776 | . . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑁 ↑m 𝐼) = (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)})))) | 
| 64 | 63 | rabeqdv 3451 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (𝑁 ↑m 𝐼) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈ Fin} = {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin}) | 
| 65 | 46, 64 | eqtr3d 2778 | . . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑘 ∈ (𝑁 ↑m 𝐼) ∣ 𝑘 finSupp 0 } = {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin}) | 
| 66 | 9, 65 | eqtrid 2788 | . 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = {𝑘 ∈ (Base‘(𝑅Xs(𝐼 × {(ringLMod‘𝑅)}))) ∣ dom (𝑘 ∖ (0g ∘ (𝐼 × {(ringLMod‘𝑅)}))) ∈
Fin}) | 
| 67 |  | frlmval.f | . . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) | 
| 68 | 67 | frlmval 21769 | . . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹 = (𝑅 ⊕m (𝐼 × {(ringLMod‘𝑅)}))) | 
| 69 | 68 | fveq2d 6909 | . 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝐹) = (Base‘(𝑅 ⊕m (𝐼 × {(ringLMod‘𝑅)})))) | 
| 70 | 8, 66, 69 | 3eqtr4d 2786 | 1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = (Base‘𝐹)) |