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	6 7	unexd	|- ( ph -> ( E u. F ) e. _V )
26		wrdexg	|- ( ( E u. F ) e. _V -> Word ( E u. F ) e. _V )
27	25 26	syl	|- ( ph -> Word ( E u. F ) e. _V )
28	27	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 ) ) ) ) ) -> Word ( E u. F ) e. _V )
29		zex	|- ZZ e. _V
30	29	a1i	|- ( ( ( ( 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 ) ) ) ) ) -> ZZ e. _V )
31		elrabi	|- ( g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } -> g e. ( ZZ ^m Word ( E u. F ) ) )
32	31	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 ) ) )
33	28 30 32	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 )
34		breq1	|- ( h = g -> ( h finSupp 0 <-> g finSupp 0 ) )
35	34	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 ) )
36	35	simprbi	|- ( g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } -> g finSupp 0 )
37	36	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 )
38		fveq2	|- ( v = w -> ( g ` v ) = ( g ` w ) )
39		oveq2	|- ( v = w -> ( ( mulGrp ` R ) gsum v ) = ( ( mulGrp ` R ) gsum w ) )
40	38 39	oveq12d	|- ( v = w -> ( ( g ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
41	40	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 ) ) )
42	41	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 ) ) ) )
43	42	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 ) ) ) ) )
44	43	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 ) ) ) ) ) )
45	44	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 ) ) ) ) )
46	1 2 3 4 8 9 10 24 33 37 45	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 ) ) ) ) )
47		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
48		eqid	|- ( .g ` R ) = ( .g ` R )
49		breq1	|- ( h = i -> ( h finSupp 0 <-> i finSupp 0 ) )
50	49	cbvrabv	|- { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } = { i e. ( ZZ ^m Word ( E u. F ) ) | i finSupp 0 }
51	1 47 48 4 50 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 ) ) ) ) ) )
52	51	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 ) ) ) ) )
53	46 52	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 ) ) ) ) )
54	5	ad3antrrr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> R e. CRing )
55	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 ) )
56	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 ) )
57	6 7	elmapd	|- ( ph -> ( p e. ( E ^m F ) <-> p : F --> E ) )
58	57	biimpa	|- ( ( ph /\ p e. ( E ^m F ) ) -> p : F --> E )
59	58	ad2antrr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> p : F --> E )
60		simplr	|- ( ( ( ( ph /\ p e. ( E ^m F ) ) /\ p finSupp .0. ) /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) -> p finSupp .0. )
61		fveq2	|- ( f = h -> ( p ` f ) = ( p ` h ) )
62		id	|- ( f = h -> f = h )
63	61 62	oveq12d	|- ( f = h -> ( ( p ` f ) .x. f ) = ( ( p ` h ) .x. h ) )
64	63	cbvmptv	|- ( f e. F |-> ( ( p ` f ) .x. f ) ) = ( h e. F |-> ( ( p ` h ) .x. h ) )
65	64	oveq2i	|- ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) = ( R gsum ( h e. F |-> ( ( p ` h ) .x. h ) ) )
66	65	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 ) ) ) )
67	66	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 ) ) ) ) )
68	67	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 ) ) ) )
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 e. ( p supp .0. ) |-> <" ( p ` f ) f "> ) = ( g e. ( p supp .0. ) |-> <" ( p ` g ) g "> )
73	72	rneqi	|- ran ( f e. ( p supp .0. ) |-> <" ( p ` f ) f "> ) = ran ( g e. ( p supp .0. ) |-> <" ( p ` g ) g "> )
74	1 2 3 4 54 55 56 59 60 68 73	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 ) ) )
75	74	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 ) ) )
76	75	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 ) ) )
77	53 76	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 ) ) ) ) ) )