This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .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 ) ) ) ) ) )