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	|- .x. = ( .r ` R )
	elrgspnsubrun.z	|- .0. = ( 0g ` R )
	elrgspnsubrun.n	|- N = ( RingSpan ` R )
	elrgspnsubrun.r	|- ( ph -> R e. CRing )
	elrgspnsubrun.e	|- ( ph -> E e. ( SubRing ` R ) )
	elrgspnsubrun.f	|- ( ph -> F e. ( SubRing ` R ) )
Assertion	elrgspnsubrun	|- ( ph -> ( X e. ( N ` ( E u. F ) ) <-> E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elrgspnsubrun.b	|- B = ( Base ` R )
2		elrgspnsubrun.t	|- .x. = ( .r ` R )
3		elrgspnsubrun.z	|- .0. = ( 0g ` R )
4		elrgspnsubrun.n	|- N = ( RingSpan ` R )
5		elrgspnsubrun.r	|- ( ph -> R e. CRing )
6		elrgspnsubrun.e	|- ( ph -> E e. ( SubRing ` R ) )
7		elrgspnsubrun.f	|- ( ph -> F e. ( SubRing ` R ) )
8	5	ad3antrrr	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> R e. CRing )
9	6	ad3antrrr	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> E e. ( SubRing ` R ) )
10	7	ad3antrrr	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> F e. ( SubRing ` R ) )
11	5	crngringd	|- ( ph -> R e. Ring )
12	1	a1i	|- ( ph -> B = ( Base ` R ) )
13	1	subrgss	|- ( E e. ( SubRing ` R ) -> E C_ B )
14	6 13	syl	|- ( ph -> E C_ B )
15	1	subrgss	|- ( F e. ( SubRing ` R ) -> F C_ B )
16	7 15	syl	|- ( ph -> F C_ B )
17	14 16	unssd	|- ( ph -> ( E u. F ) C_ B )
18	4	a1i	|- ( ph -> N = ( RingSpan ` R ) )
19		eqidd	|- ( ph -> ( N ` ( E u. F ) ) = ( N ` ( E u. F ) ) )
20	11 12 17 18 19	rgspncl	|- ( ph -> ( N ` ( E u. F ) ) e. ( SubRing ` R ) )
21	1	subrgss	|- ( ( N ` ( E u. F ) ) e. ( SubRing ` R ) -> ( N ` ( E u. F ) ) C_ B )
22	20 21	syl	|- ( ph -> ( N ` ( E u. F ) ) C_ B )
23	22	sselda	|- ( ( ph /\ X e. ( N ` ( E u. F ) ) ) -> X e. B )
24	23	ad2antrr	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> X e. B )
25		elrabi	|- ( g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } -> g e. ( ZZ ^m Word ( E u. F ) ) )
26	25	ad2antlr	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> g e. ( ZZ ^m Word ( E u. F ) ) )
27	26	elmaprd	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> g : Word ( E u. F ) --> ZZ )
28		breq1	|- ( h = g -> ( h finSupp 0 <-> g finSupp 0 ) )
29	28	elrab	|- ( g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } <-> ( g e. ( ZZ ^m Word ( E u. F ) ) /\ g finSupp 0 ) )
30	29	simprbi	|- ( g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } -> g finSupp 0 )
31	30	ad2antlr	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> g finSupp 0 )
32		fveq2	|- ( v = w -> ( g ` v ) = ( g ` w ) )
33		oveq2	|- ( v = w -> ( ( mulGrp ` R ) gsum v ) = ( ( mulGrp ` R ) gsum w ) )
34	32 33	oveq12d	|- ( v = w -> ( ( g ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
35	34	cbvmptv	|- ( v e. Word ( E u. F ) |-> ( ( g ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) ) = ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
36	35	oveq2i	|- ( R gsum ( v e. Word ( E u. F ) |-> ( ( g ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) ) ) = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) )
37	36	a1i	|- ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) -> ( R gsum ( v e. Word ( E u. F ) |-> ( ( g ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) ) ) = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
38	37	eqeq2d	|- ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) -> ( X = ( R gsum ( v e. Word ( E u. F ) |-> ( ( g ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) ) ) <-> X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) )
39	38	biimpar	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> X = ( R gsum ( v e. Word ( E u. F ) |-> ( ( g ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) ) ) )
40	1 2 3 4 8 9 10 24 27 31 39	elrgspnsubrunlem2	|- ( ( ( ( ph /\ X e. ( N ` ( E u. F ) ) ) /\ g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } ) /\ X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) -> E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) )
41		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
42		eqid	|- ( .g ` R ) = ( .g ` R )
43		breq1	|- ( h = i -> ( h finSupp 0 <-> i finSupp 0 ) )
44	43	cbvrabv	|- { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } = { i e. ( ZZ ^m Word ( E u. F ) ) | i finSupp 0 }
45	1 41 42 4 44 11 17	elrgspn	|- ( ph -> ( X e. ( N ` ( E u. F ) ) <-> E. g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) )
46	45	biimpa	|- ( ( ph /\ X e. ( N ` ( E u. F ) ) ) -> E. g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
47	40 46	r19.29a	|- ( ( ph /\ X e. ( N ` ( E u. F ) ) ) -> E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) )
48	5	ad3antrrr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> R e. CRing )
49	6	ad3antrrr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> E e. ( SubRing ` R ) )
50	7	ad3antrrr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> F e. ( SubRing ` R ) )
51	6 7	elmapd	|- ( ph -> ( p e. ( E ^m F ) <-> p : F --> E ) )
52	51	biimpa	|- ( ( ph /\ p e. ( E ^m F ) ) -> p : F --> E )
53	52	ad2antrr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> p : F --> E )
54		simplr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> p finSupp .0. )
55		fveq2	|- ( f = h -> ( p ` f ) = ( p ` h ) )
56		id	|- ( f = h -> f = h )
57	55 56	oveq12d	|- ( f = h -> ( ( p ` f ) .x. f ) = ( ( p ` h ) .x. h ) )
58	57	cbvmptv	|- ( f e. F |-> ( ( p ` f ) .x. f ) ) = ( h e. F |-> ( ( p ` h ) .x. h ) )
59	58	oveq2i	|- ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) = ( R gsum ( h e. F |-> ( ( p ` h ) .x. h ) ) )
60	59	a1i	|- ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) -> ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) = ( R gsum ( h e. F |-> ( ( p ` h ) .x. h ) ) ) )
61	60	eqeq2d	|- ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) -> ( X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) <-> X = ( R gsum ( h e. F |-> ( ( p ` h ) .x. h ) ) ) ) )
62	61	biimpa	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> X = ( R gsum ( h e. F |-> ( ( p ` h ) .x. 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 e. ( p supp .0. ) |-> <" ( p ` f ) f "> ) = ( g e. ( p supp .0. ) |-> <" ( p ` g ) g "> )
67	66	rneqi	|- ran ( f e. ( p supp .0. ) |-> <" ( p ` f ) f "> ) = ran ( g e. ( p supp .0. ) |-> <" ( p ` g ) g "> )
68	1 2 3 4 48 49 50 53 54 62 67	elrgspnsubrunlem1	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> X e. ( N ` ( E u. F ) ) )
69	68	anasss	|- ( ( ( ph /\ p e. ( E ^m F ) ) /\ ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) ) -> X e. ( N ` ( E u. F ) ) )
70	69	r19.29an	|- ( ( ph /\ E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) ) -> X e. ( N ` ( E u. F ) ) )
71	47 70	impbida	|- ( ph -> ( X e. ( N ` ( E u. F ) ) <-> E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) ) )