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 6 7 unexd ⊢ φ → E ∪ F ∈ V
26 wrdexg ⊢ E ∪ F ∈ V → Word E ∪ F ∈ V
27 25 26 syl ⊢ φ → Word E ∪ F ∈ V
28 27 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 → Word E ∪ F ∈ V
29 zex ⊢ ℤ ∈ V
30 29 a1i ⊢ φ ∧ X ∈ N ⁡ E ∪ F ∧ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ∧ X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w → ℤ ∈ V
31 elrabi ⊢ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h → g ∈ ℤ Word E ∪ F
32 31 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
33 28 30 32 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 ⟶ ℤ
34 breq1 ⊢ h = g → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ g
35 34 elrab ⊢ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h ↔ g ∈ ℤ Word E ∪ F ∧ finSupp 0 ⁡ g
36 35 simprbi ⊢ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h → finSupp 0 ⁡ g
37 36 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
38 fveq2 ⊢ v = w → g ⁡ v = g ⁡ w
39 oveq2 ⊢ v = w → ∑ mulGrp R v = ∑ mulGrp R w
40 38 39 oveq12d ⊢ v = w → g ⁡ v ⋅ R ∑ mulGrp R v = g ⁡ w ⋅ R ∑ mulGrp R w
41 40 cbvmptv ⊢ v ∈ Word E ∪ F ⟼ g ⁡ v ⋅ R ∑ mulGrp R v = w ∈ Word E ∪ F ⟼ g ⁡ w ⋅ R ∑ mulGrp R w
42 41 oveq2i ⊢ ∑ R v ∈ Word E ∪ F g ⁡ v ⋅ R ∑ mulGrp R v = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
43 42 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
44 43 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
45 44 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
46 1 2 3 4 8 9 10 24 33 37 45 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
47 eqid ⊢ mulGrp R = mulGrp R
48 eqid ⊢ ⋅ R = ⋅ R
49 breq1 ⊢ h = i → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ i
50 49 cbvrabv ⊢ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h = i ∈ ℤ Word E ∪ F | finSupp 0 ⁡ i
51 1 47 48 4 50 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
52 51 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
53 46 52 r19.29a ⊢ φ ∧ X ∈ N ⁡ E ∪ F → ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f
54 5 ad3antrrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → R ∈ CRing
55 6 ad3antrrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → E ∈ SubRing ⁡ R
56 7 ad3antrrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → F ∈ SubRing ⁡ R
57 6 7 elmapd ⊢ φ → p ∈ E F ↔ p : F ⟶ E
58 57 biimpa ⊢ φ ∧ p ∈ E F → p : F ⟶ E
59 58 ad2antrr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → p : F ⟶ E
60 simplr ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → finSupp 0 ˙⁡ p
61 fveq2 ⊢ f = h → p ⁡ f = p ⁡ h
62 id ⊢ f = h → f = h
63 61 62 oveq12d ⊢ f = h → p ⁡ f · ˙ f = p ⁡ h · ˙ h
64 63 cbvmptv ⊢ f ∈ F ⟼ p ⁡ f · ˙ f = h ∈ F ⟼ p ⁡ h · ˙ h
65 64 oveq2i ⊢ ∑ R f ∈ F p ⁡ f · ˙ f = ∑ R h ∈ F p ⁡ h · ˙ h
66 65 a1i ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p → ∑ R f ∈ F p ⁡ f · ˙ f = ∑ R h ∈ F p ⁡ h · ˙ h
67 66 eqeq2d ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p → X = ∑ R f ∈ F p ⁡ f · ˙ f ↔ X = ∑ R h ∈ F p ⁡ h · ˙ h
68 67 biimpa ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X = ∑ R h ∈ F p ⁡ h · ˙ h
69 fveq2 ⊢ f = g → p ⁡ f = p ⁡ g
70 id ⊢ f = g → f = g
71 69 70 s2eqd ⊢ f = g → ⟨“ p ⁡ f f ”⟩ = ⟨“ p ⁡ g g ”⟩
72 71 cbvmptv ⊢ f ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ f f ”⟩ = g ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ g g ”⟩
73 72 rneqi ⊢ ran ⁡ f ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ f f ”⟩ = ran ⁡ g ∈ supp 0 ˙⁡ p ⟼ ⟨“ p ⁡ g g ”⟩
74 1 2 3 4 54 55 56 59 60 68 73 elrgspnsubrunlem1 ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X ∈ N ⁡ E ∪ F
75 74 anasss ⊢ φ ∧ p ∈ E F ∧ finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X ∈ N ⁡ E ∪ F
76 75 r19.29an ⊢ φ ∧ ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f → X ∈ N ⁡ E ∪ F
77 53 76 impbida ⊢ φ → X ∈ N ⁡ E ∪ F ↔ ∃ p ∈ E F finSupp 0 ˙⁡ p ∧ X = ∑ R f ∈ F p ⁡ f · ˙ f