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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
elrgspnsubrun.t ⊢ · = ( .r ‘ 𝑅 )
elrgspnsubrun.z ⊢ 0 = ( 0g ‘ 𝑅 )
elrgspnsubrun.n ⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
elrgspnsubrun.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
elrgspnsubrun.e ⊢ ( 𝜑 → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
elrgspnsubrun.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
Assertion elrgspnsubrun ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ↔ ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elrgspnsubrun.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 elrgspnsubrun.t ⊢ · = ( .r ‘ 𝑅 )
3 elrgspnsubrun.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 elrgspnsubrun.n ⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
5 elrgspnsubrun.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 elrgspnsubrun.e ⊢ ( 𝜑 → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
7 elrgspnsubrun.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
8 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑅 ∈ CRing )
9 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
10 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
11 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
12 1 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
13 1 subrgss ⊢ ( 𝐸 ∈ ( SubRing ‘ 𝑅 ) → 𝐸 ⊆ 𝐵 )
14 6 13 syl ⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
15 1 subrgss ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝑅 ) → 𝐹 ⊆ 𝐵 )
16 7 15 syl ⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
17 14 16 unssd ⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ⊆ 𝐵 )
18 4 a1i ⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
19 eqidd ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) = ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )
20 11 12 17 18 19 rgspncl ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ∈ ( SubRing ‘ 𝑅 ) )
21 1 subrgss ⊢ ( ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ∈ ( SubRing ‘ 𝑅 ) → ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ⊆ 𝐵 )
22 20 21 syl ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ⊆ 𝐵 )
23 22 sselda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) → 𝑋 ∈ 𝐵 )
24 23 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑋 ∈ 𝐵 )
25 6 7 unexd ⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ∈ V )
26 wrdexg ⊢ ( ( 𝐸 ∪ 𝐹 ) ∈ V → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
27 25 26 syl ⊢ ( 𝜑 → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
28 27 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
29 zex ⊢ ℤ ∈ V
30 29 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → ℤ ∈ V )
31 elrabi ⊢ ( 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } → 𝑔 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) )
32 31 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑔 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) )
33 28 30 32 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑔 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
34 breq1 ⊢ ( ℎ = 𝑔 → ( ℎ finSupp 0 ↔ 𝑔 finSupp 0 ) )
35 34 elrab ⊢ ( 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ↔ ( 𝑔 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑔 finSupp 0 ) )
36 35 simprbi ⊢ ( 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } → 𝑔 finSupp 0 )
37 36 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑔 finSupp 0 )
38 fveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝑔 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑤 ) )
39 oveq2 ⊢ ( 𝑣 = 𝑤 → ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) = ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) )
40 38 39 oveq12d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) = ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) )
41 40 cbvmptv ⊢ ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) = ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) )
42 41 oveq2i ⊢ ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) )
43 42 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) → ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) )
44 43 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) → ( 𝑋 = ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) ↔ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) )
45 44 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑋 = ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) )
46 1 2 3 4 8 9 10 24 33 37 45 elrgspnsubrunlem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) )
47 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
48 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
49 breq1 ⊢ ( ℎ = 𝑖 → ( ℎ finSupp 0 ↔ 𝑖 finSupp 0 ) )
50 49 cbvrabv ⊢ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } = { 𝑖 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ 𝑖 finSupp 0 }
51 1 47 48 4 50 11 17 elrgspn ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ↔ ∃ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) )
52 51 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) → ∃ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) )
53 46 52 r19.29a ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) → ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) )
54 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑅 ∈ CRing )
55 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
56 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
57 6 7 elmapd ⊢ ( 𝜑 → ( 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ↔ 𝑝 : 𝐹 ⟶ 𝐸 ) )
58 57 biimpa ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) → 𝑝 : 𝐹 ⟶ 𝐸 )
59 58 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑝 : 𝐹 ⟶ 𝐸 )
60 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑝 finSupp 0 )
61 fveq2 ⊢ ( 𝑓 = ℎ → ( 𝑝 ‘ 𝑓 ) = ( 𝑝 ‘ ℎ ) )
62 id ⊢ ( 𝑓 = ℎ → 𝑓 = ℎ )
63 61 62 oveq12d ⊢ ( 𝑓 = ℎ → ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) = ( ( 𝑝 ‘ ℎ ) · ℎ ) )
64 63 cbvmptv ⊢ ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) = ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) )
65 64 oveq2i ⊢ ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) )
66 65 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) → ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) ) )
67 66 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) → ( 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ↔ 𝑋 = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) ) ) )
68 67 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑋 = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) ) )
69 fveq2 ⊢ ( 𝑓 = 𝑔 → ( 𝑝 ‘ 𝑓 ) = ( 𝑝 ‘ 𝑔 ) )
70 id ⊢ ( 𝑓 = 𝑔 → 𝑓 = 𝑔 )
71 69 70 s2eqd ⊢ ( 𝑓 = 𝑔 → ⟨“ ( 𝑝 ‘ 𝑓 ) 𝑓 ”⟩ = ⟨“ ( 𝑝 ‘ 𝑔 ) 𝑔 ”⟩ )
72 71 cbvmptv ⊢ ( 𝑓 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑓 ) 𝑓 ”⟩ ) = ( 𝑔 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑔 ) 𝑔 ”⟩ )
73 72 rneqi ⊢ ran ( 𝑓 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑓 ) 𝑓 ”⟩ ) = ran ( 𝑔 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑔 ) 𝑔 ”⟩ )
74 1 2 3 4 54 55 56 59 60 68 73 elrgspnsubrunlem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )
75 74 anasss ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )
76 75 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )
77 53 76 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ↔ ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ) )