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 elrabi ⊢ ( 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } → 𝑔 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) )
26 25 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑔 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) )
27 26 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑔 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
28 breq1 ⊢ ( ℎ = 𝑔 → ( ℎ finSupp 0 ↔ 𝑔 finSupp 0 ) )
29 28 elrab ⊢ ( 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ↔ ( 𝑔 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑔 finSupp 0 ) )
30 29 simprbi ⊢ ( 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } → 𝑔 finSupp 0 )
31 30 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑔 finSupp 0 )
32 fveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝑔 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑤 ) )
33 oveq2 ⊢ ( 𝑣 = 𝑤 → ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) = ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) )
34 32 33 oveq12d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) = ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) )
35 34 cbvmptv ⊢ ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) = ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) )
36 35 oveq2i ⊢ ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) )
37 36 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) → ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) )
38 37 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) → ( 𝑋 = ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) ↔ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) )
39 38 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → 𝑋 = ( 𝑅 Σg ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑣 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑣 ) ) ) ) )
40 1 2 3 4 8 9 10 24 27 31 39 elrgspnsubrunlem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) → ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) )
41 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
42 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
43 breq1 ⊢ ( ℎ = 𝑖 → ( ℎ finSupp 0 ↔ 𝑖 finSupp 0 ) )
44 43 cbvrabv ⊢ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } = { 𝑖 ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ 𝑖 finSupp 0 }
45 1 41 42 4 44 11 17 elrgspn ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ↔ ∃ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) ) )
46 45 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) → ∃ 𝑔 ∈ { ℎ ∈ ( ℤ ↑m Word ( 𝐸 ∪ 𝐹 ) ) ∣ ℎ finSupp 0 } 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝑔 ‘ 𝑤 ) ( .g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg 𝑤 ) ) ) ) )
47 40 46 r19.29a ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ) → ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) )
48 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑅 ∈ CRing )
49 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
50 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
51 6 7 elmapd ⊢ ( 𝜑 → ( 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ↔ 𝑝 : 𝐹 ⟶ 𝐸 ) )
52 51 biimpa ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) → 𝑝 : 𝐹 ⟶ 𝐸 )
53 52 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑝 : 𝐹 ⟶ 𝐸 )
54 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑝 finSupp 0 )
55 fveq2 ⊢ ( 𝑓 = ℎ → ( 𝑝 ‘ 𝑓 ) = ( 𝑝 ‘ ℎ ) )
56 id ⊢ ( 𝑓 = ℎ → 𝑓 = ℎ )
57 55 56 oveq12d ⊢ ( 𝑓 = ℎ → ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) = ( ( 𝑝 ‘ ℎ ) · ℎ ) )
58 57 cbvmptv ⊢ ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) = ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) )
59 58 oveq2i ⊢ ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) )
60 59 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) → ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) ) )
61 60 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) → ( 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ↔ 𝑋 = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) ) ) )
62 61 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑋 = ( 𝑅 Σg ( ℎ ∈ 𝐹 ↦ ( ( 𝑝 ‘ ℎ ) · ℎ ) ) ) )
63 fveq2 ⊢ ( 𝑓 = 𝑔 → ( 𝑝 ‘ 𝑓 ) = ( 𝑝 ‘ 𝑔 ) )
64 id ⊢ ( 𝑓 = 𝑔 → 𝑓 = 𝑔 )
65 63 64 s2eqd ⊢ ( 𝑓 = 𝑔 → ⟨“ ( 𝑝 ‘ 𝑓 ) 𝑓 ”⟩ = ⟨“ ( 𝑝 ‘ 𝑔 ) 𝑔 ”⟩ )
66 65 cbvmptv ⊢ ( 𝑓 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑓 ) 𝑓 ”⟩ ) = ( 𝑔 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑔 ) 𝑔 ”⟩ )
67 66 rneqi ⊢ ran ( 𝑓 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑓 ) 𝑓 ”⟩ ) = ran ( 𝑔 ∈ ( 𝑝 supp 0 ) ↦ ⟨“ ( 𝑝 ‘ 𝑔 ) 𝑔 ”⟩ )
68 1 2 3 4 48 49 50 53 54 62 67 elrgspnsubrunlem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ 𝑝 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )
69 68 anasss ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ) ∧ ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )
70 69 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )
71 47 70 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) ↔ ∃ 𝑝 ∈ ( 𝐸 ↑m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σg ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ) )