Metamath Proof Explorer

Theorem elrgspnsubrun

Description: Membership in the ring span of the union of two subrings of a commutative ring. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses elrgspnsubrun.b ⊢ B = Base R
elrgspnsubrun.t ⊢ · ˙ = ⋅ R
elrgspnsubrun.z ⊢ 0 ˙ = 0 R
elrgspnsubrun.n ⊢ N = RingSpan ⁡ R
elrgspnsubrun.r ⊢ φ → R ∈ CRing
elrgspnsubrun.e ⊢ φ → E ∈ SubRing ⁡ R
elrgspnsubrun.f ⊢ φ → F ∈ SubRing ⁡ R
Assertion elrgspnsubrun ⊢ φ → X ∈ N ⁡ E ∪ F ↔ ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f

Proof

Step Hyp Ref Expression
1 elrgspnsubrun.b ⊢ B = Base R
2 elrgspnsubrun.t ⊢ · ˙ = ⋅ R
3 elrgspnsubrun.z ⊢ 0 ˙ = 0 R
4 elrgspnsubrun.n ⊢ N = RingSpan ⁡ R
5 elrgspnsubrun.r ⊢ φ → R ∈ CRing
6 elrgspnsubrun.e ⊢ φ → E ∈ SubRing ⁡ R
7 elrgspnsubrun.f ⊢ φ → F ∈ SubRing ⁡ R
8 5 ad3antrrr ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → R ∈ CRing
9 6 ad3antrrr ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → E ∈ SubRing ⁡ R
10 7 ad3antrrr ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → F ∈ SubRing ⁡ R
11 5 crngringd ⊢ φ → R ∈ Ring
12 1 a1i ⊢ φ → B = Base R
13 1 subrgss ⊢ E ∈ SubRing ⁡ R → E ⊆ B
14 6 13 syl ⊢ φ → E ⊆ B
15 1 subrgss ⊢ F ∈ SubRing ⁡ R → F ⊆ B
16 7 15 syl ⊢ φ → F ⊆ B
17 14 16 unssd ⊢ φ → E ∪ F ⊆ B
18 4 a1i ⊢ φ → N = RingSpan ⁡ R
19 eqidd ⊢ φ → N ⁡ E ∪ F = N ⁡ E ∪ F
20 11 12 17 18 19 rgspncl ⊢ φ → N ⁡ E ∪ F ∈ SubRing ⁡ R
21 1 subrgss ⊢ N ⁡ E ∪ F ∈ SubRing ⁡ R → N ⁡ E ∪ F ⊆ B
22 20 21 syl ⊢ φ → N ⁡ E ∪ F ⊆ B
23 22 sselda ⊢ φ ∧ X ∈ N ⁡ E ∪ F → X ∈ B
24 23 ad2antrr ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → X ∈ B
25 elrabi ⊢ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h → g ∈ ℤ Word E ∪ F
26 25 ad2antlr ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → g ∈ ℤ Word E ∪ F
27 26 elmaprd ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → g : Word E ∪ F ⟶ ℤ
28 breq1 ⊢ h = g → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ g
29 28 elrab ⊢ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ↔ g ∈ ℤ Word E ∪ F ∧ finSupp 0 ⁡ g
30 29 simprbi ⊢ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h → finSupp 0 ⁡ g
31 30 ad2antlr ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → finSupp 0 ⁡ g
32 fveq2 ⊢ v = w → g ⁡ v = g ⁡ w
33 oveq2 ⊢ v = w → ∑ mulGrp R v = ∑ mulGrp R w
34 32 33 oveq12d ⊢ v = w → g ⁡ v ⋅ R ∑ mulGrp R v = g ⁡ w ⋅ R ∑ mulGrp R w
35 34 cbvmptv ⊢ v ∈ Word E ∪ F ⟼ g ⁡ v ⋅ R ∑ mulGrp R v = w ∈ Word E ∪ F ⟼ g ⁡ w ⋅ R ∑ mulGrp R w
36 35 oveq2i ⊢ ∑ R v ∈ Word E ∪ F g ⁡ v ⋅ R ∑ mulGrp R v = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
37 36 a1i ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h → ∑ R v ∈ Word E ∪ F g ⁡ v ⋅ R ∑ mulGrp R v = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
38 37 eqeq2d ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h → X = ∑ R v ∈ Word E ∪ F g ⁡ v ⋅ R ∑ mulGrp R v ↔ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
39 38 biimpar ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → X = ∑ R v ∈ Word E ∪ F g ⁡ v ⋅ R ∑ mulGrp R v
40 1 2 3 4 8 9 10 24 27 31 39 elrgspnsubrunlem2 ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f
41 eqid ⊢ mulGrp R = mulGrp R
42 eqid ⊢ ⋅ R = ⋅ R
43 breq1 ⊢ h = i → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ i
44 43 cbvrabv ⊢ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h = i ∈ ℤ Word E ∪ F | finSupp 0 ⁡ i
45 1 41 42 4 44 11 17 elrgspn ⊢ φ → X ∈ N ⁡ E ∪ F ↔ ∃ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
46 45 biimpa ⊢ φ ∧ X ∈ N ⁡ E ∪ F → ∃ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
47 40 46 r19.29a ⊢ φ ∧ X ∈ N ⁡ E ∪ F → ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f
48 5 ad3antrrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → R ∈ CRing
49 6 ad3antrrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → E ∈ SubRing ⁡ R
50 7 ad3antrrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → F ∈ SubRing ⁡ R
51 6 7 elmapd ⊢ φ → p ∈ E F ↔ p : F ⟶ E
52 51 biimpa ⊢ φ ∧ p ∈ E F → p : F ⟶ E
53 52 ad2antrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → p : F ⟶ E
54 simplr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → finSupp 0 ˙⁡ p
55 fveq2 ⊢ f = h → p ⁡ f = p ⁡ h
56 id ⊢ f = h → f = h
57 55 56 oveq12d ⊢ f = h → p ⁡ f · ˙ f = p ⁡ h · ˙ h
58 57 cbvmptv ⊢ f ∈ F ⟼ p ⁡ f · ˙ f = h ∈ F ⟼ p ⁡ h · ˙ h
59 58 oveq2i ⊢ ∑ R f ∈ F p ⁡ f · ˙ f = ∑ R h ∈ F p ⁡ h · ˙ h
60 59 a1i ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p → ∑ R f ∈ F p ⁡ f · ˙ f = ∑ R h ∈ F p ⁡ h · ˙ h
61 60 eqeq2d ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p → X = ∑ R f ∈ F p ⁡ f · ˙ f ↔ X = ∑ R h ∈ F p ⁡ h · ˙ h
62 61 biimpa ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X = ∑ R h ∈ F p ⁡ h · ˙ h
63 fveq2 ⊢ f = g → p ⁡ f = p ⁡ g
64 id ⊢ f = g → f = g
65 63 64 s2eqd ⊢ f = g → ⟨“ p ⁡ f f ”⟩ = ⟨“ p ⁡ g g ”⟩
66 65 cbvmptv ⊢ f ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ f f ”⟩ = g ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ g g ”⟩
67 66 rneqi ⊢ ran ⁡ f ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ f f ”⟩ = ran ⁡ g ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ g g ”⟩
68 1 2 3 4 48 49 50 53 54 62 67 elrgspnsubrunlem1 ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X ∈ N ⁡ E ∪ F
69 68 anasss ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X ∈ N ⁡ E ∪ F
70 69 r19.29an ⊢ φ ∧ ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X ∈ N ⁡ E ∪ F
71 47 70 impbida ⊢ φ → X ∈ N ⁡ E ∪ F ↔ ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f