Metamath Proof Explorer

Theorem elrsp

Description: Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses elrsp.n ⊢ 𝑁 = ( RSpan ‘ 𝑅 )
elrsp.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
elrsp.1 ⊢ 0 = ( 0g ‘ 𝑅 )
elrsp.x ⊢ · = ( .r ‘ 𝑅 )
elrsp.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
elrsp.i ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
Assertion elrsp ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝐼 ) ↔ ∃ 𝑎 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elrsp.n ⊢ 𝑁 = ( RSpan ‘ 𝑅 )
2 elrsp.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 elrsp.1 ⊢ 0 = ( 0g ‘ 𝑅 )
4 elrsp.x ⊢ · = ( .r ‘ 𝑅 )
5 elrsp.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 elrsp.i ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
7 rspval ⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
8 1 7 eqtri ⊢ 𝑁 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
9 rlmbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
10 2 9 eqtri ⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
11 eqid ⊢ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
12 eqid ⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
13 eqid ⊢ ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
14 rlmvsca ⊢ ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
15 4 14 eqtri ⊢ · = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
16 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
17 5 16 syl ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ LMod )
18 8 10 11 12 13 15 17 6 ellspds ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝐼 ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ↑m 𝐼 ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ 𝑋 = ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) ) )
19 rlmsca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
20 5 19 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
22 2 21 syl5eq ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( 𝐵 ↑m 𝐼 ) = ( ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ↑m 𝐼 ) )
24 20 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
25 3 24 syl5eq ⊢ ( 𝜑 → 0 = ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
26 25 breq2d ⊢ ( 𝜑 → ( 𝑎 finSupp 0 ↔ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ) )
27 2 fvexi ⊢ 𝐵 ∈ V
28 27 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
29 28 6 ssexd ⊢ ( 𝜑 → 𝐼 ∈ V )
30 29 mptexd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ∈ V )
31 9 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
32 rlmplusg ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
33 32 a1i ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) ) )
34 30 5 17 31 33 gsumpropd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) = ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) )
35 34 eqeq2d ⊢ ( 𝜑 → ( 𝑋 = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ↔ 𝑋 = ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) )
36 26 35 anbi12d ⊢ ( 𝜑 → ( ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) ↔ ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ 𝑋 = ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) ) )
37 23 36 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ↑m 𝐼 ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ 𝑋 = ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) ) )
38 18 37 bitr4d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝐼 ) ↔ ∃ 𝑎 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑖 ) · 𝑖 ) ) ) ) ) )