Metamath Proof Explorer

Theorem frlmbas

Description: Base set of the free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 23-Jun-2019)

Ref Expression
Hypotheses frlmval.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmbas.n ⊢ 𝑁 = ( Base ‘ 𝑅 )
frlmbas.z ⊢ 0 = ( 0g ‘ 𝑅 )
frlmbas.b ⊢ 𝐵 = { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 }
Assertion frlmbas ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 = ( Base ‘ 𝐹 ) )

Proof

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 ‘ 𝐹 ) )