ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mplsubgfilemcl Unicode version
Theorem mplsubgfilemcl 15246
Description: Lemma for mplsubgfi 15248. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
Hypotheses
Ref Expression
mplsubg.s |- S = ( I mPwSer R )
mplsubg.p |- P = ( I mPoly R )
mplsubg.u |- U = ( Base ` P )
mplsubg.i |- ( ph -> I e. Fin )
mplsubg.r |- ( ph -> R e. Grp )
mplsubgfilemcl.x |- ( ph -> X e. U )
mplsubgfilemcl.y |- ( ph -> Y e. U )
mplsubgfilemcl.p |- .+ = ( +g ` S )
Assertion
Ref Expression
mplsubgfilemcl |- ( ph -> ( X .+ Y ) e. U )
Proof of Theorem mplsubgfilemcl
Dummy variables a b c p q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplsubg.s . . 3 |- S = ( I mPwSer R )
2 eqid 2238 . . 3 |- ( Base ` S ) = ( Base ` S )
3 mplsubgfilemcl.p . . 3 |- .+ = ( +g ` S )
4 mplsubg.r . . . 4 |- ( ph -> R e. Grp )
54grpmgmd 13890 . . 3 |- ( ph -> R e. Mgm )
6 mplsubg.p . . . . 5 |- P = ( I mPoly R )
7 mplsubg.u . . . . 5 |- U = ( Base ` P )
86, 1, 7, 2mplbasss 15243 . . . 4 |- U C_ ( Base ` S )
9 mplsubgfilemcl.x . . . 4 |- ( ph -> X e. U )
108, 9sselid 3246 . . 3 |- ( ph -> X e. ( Base ` S ) )
11 mplsubgfilemcl.y . . . 4 |- ( ph -> Y e. U )
128, 11sselid 3246 . . 3 |- ( ph -> Y e. ( Base ` S ) )
131, 2, 3, 5, 10, 12psraddcl 15203 . 2 |- ( ph -> ( X .+ Y ) e. ( Base ` S ) )
14 eqid 2238 . . . . . . 7 |- ( 0g ` R ) = ( 0g ` R )
156, 1, 2, 14, 7mplelbas 15236 . . . . . 6 |- ( X e. U <-> ( X e. ( Base ` S ) /\ X finSupp ( 0g ` R ) ) )
169, 15sylib 122 . . . . 5 |- ( ph -> ( X e. ( Base ` S ) /\ X finSupp ( 0g ` R ) ) )
1716simprd 114 . . . 4 |- ( ph -> X finSupp ( 0g ` R ) )
1817fsuppfiss 7301 . . 3 |- ( ph -> E. a ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) )
196, 1, 2, 14, 7mplelbas 15236 . . . . . . . 8 |- ( Y e. U <-> ( Y e. ( Base ` S ) /\ Y finSupp ( 0g ` R ) ) )
2011, 19sylib 122 . . . . . . 7 |- ( ph -> ( Y e. ( Base ` S ) /\ Y finSupp ( 0g ` R ) ) )
2120simprd 114 . . . . . 6 |- ( ph -> Y finSupp ( 0g ` R ) )
2221fsuppfiss 7301 . . . . 5 |- ( ph -> E. b ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) )
2322adantr 276 . . . 4 |- ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) -> E. b ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) )
24 simplr2 1071 . . . . . . 7 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> a C_ dom X )
25 eqid 2238 . . . . . . . . . . 11 |- ( Base ` R ) = ( Base ` R )
26 mplsubg.i . . . . . . . . . . 11 |- ( ph -> I e. Fin )
271, 25, 26, 2, 10psrelbasfi 15199 . . . . . . . . . 10 |- ( ph -> X : ( NN0 ^m I ) --> ( Base ` R ) )
2827fdmd 5543 . . . . . . . . 9 |- ( ph -> dom X = ( NN0 ^m I ) )
2928sseq2d 3278 . . . . . . . 8 |- ( ph -> ( a C_ dom X <-> a C_ ( NN0 ^m I ) ) )
3029ad2antrr 492 . . . . . . 7 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> ( a C_ dom X <-> a C_ ( NN0 ^m I ) ) )
3124, 30mpbid 147 . . . . . 6 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> a C_ ( NN0 ^m I ) )
32 simplr1 1070 . . . . . 6 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> a e. Fin )
33 simpr2 1035 . . . . . . 7 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> b C_ dom Y )
341, 25, 26, 2, 12psrelbasfi 15199 . . . . . . . . . 10 |- ( ph -> Y : ( NN0 ^m I ) --> ( Base ` R ) )
3534fdmd 5543 . . . . . . . . 9 |- ( ph -> dom Y = ( NN0 ^m I ) )
3635sseq2d 3278 . . . . . . . 8 |- ( ph -> ( b C_ dom Y <-> b C_ ( NN0 ^m I ) ) )
3736ad2antrr 492 . . . . . . 7 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> ( b C_ dom Y <-> b C_ ( NN0 ^m I ) ) )
3833, 37mpbid 147 . . . . . 6 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> b C_ ( NN0 ^m I ) )
39 simpr1 1034 . . . . . 6 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> b e. Fin )
4026ad2antrr 492 . . . . . 6 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> I e. Fin )
4131, 32, 38, 39, 40psrbagmax 15190 . . . . 5 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> E. c ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) )
4213ad3antrrr 496 . . . . . 6 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( X .+ Y ) e. ( Base ` S ) )
4325, 14grpidcl 13893 . . . . . . . 8 |- ( R e. Grp -> ( 0g ` R ) e. ( Base ` R ) )
444, 43syl 14 . . . . . . 7 |- ( ph -> ( 0g ` R ) e. ( Base ` R ) )
4544ad3antrrr 496 . . . . . 6 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( 0g ` R ) e. ( Base ` R ) )
461, 25, 26, 2, 13psrelbasfi 15199 . . . . . . . 8 |- ( ph -> ( X .+ Y ) : ( NN0 ^m I ) --> ( Base ` R ) )
4746ffund 5540 . . . . . . 7 |- ( ph -> Fun ( X .+ Y ) )
4847ad3antrrr 496 . . . . . 6 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> Fun ( X .+ Y ) )
49 simprlr 544 . . . . . 6 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> c e. Fin )
50 simprll 543 . . . . . . 7 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> c C_ ( NN0 ^m I ) )
5146fdmd 5543 . . . . . . . . 9 |- ( ph -> dom ( X .+ Y ) = ( NN0 ^m I ) )
5251sseq2d 3278 . . . . . . . 8 |- ( ph -> ( c C_ dom ( X .+ Y ) <-> c C_ ( NN0 ^m I ) ) )
5352ad3antrrr 496 . . . . . . 7 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( c C_ dom ( X .+ Y ) <-> c C_ ( NN0 ^m I ) ) )
5450, 53mpbird 167 . . . . . 6 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> c C_ dom ( X .+ Y ) )
55 fvelima 5757 . . . . . . . . . 10 |- ( ( Fun ( X .+ Y ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) -> E. q e. ( dom ( X .+ Y ) \ c ) ( ( X .+ Y ) ` q ) = p )
5648, 55sylan 283 . . . . . . . . 9 |- ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) -> E. q e. ( dom ( X .+ Y ) \ c ) ( ( X .+ Y ) ` q ) = p )
57 eqid 2238 . . . . . . . . . . . . . . 15 |- ( +g ` R ) = ( +g ` R )
581, 2, 57, 3, 10, 12psradd 15202 . . . . . . . . . . . . . 14 |- ( ph -> ( X .+ Y ) = ( X oF ( +g ` R ) Y ) )
5958fveq1d 5700 . . . . . . . . . . . . 13 |- ( ph -> ( ( X .+ Y ) ` q ) = ( ( X oF ( +g ` R ) Y ) ` q ) )
6059ad5antr 500 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( ( X .+ Y ) ` q ) = ( ( X oF ( +g ` R ) Y ) ` q ) )
61 simp-5l 549 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ph )
62 simprl 535 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> q e. ( dom ( X .+ Y ) \ c ) )
6362eldifad 3231 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> q e. dom ( X .+ Y ) )
6451eleq2d 2308 . . . . . . . . . . . . . . 15 |- ( ph -> ( q e. dom ( X .+ Y ) <-> q e. ( NN0 ^m I ) ) )
6564ad5antr 500 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( q e. dom ( X .+ Y ) <-> q e. ( NN0 ^m I ) ) )
6663, 65mpbid 147 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> q e. ( NN0 ^m I ) )
6727ffnd 5537 . . . . . . . . . . . . . 14 |- ( ph -> X Fn ( NN0 ^m I ) )
6834ffnd 5537 . . . . . . . . . . . . . 14 |- ( ph -> Y Fn ( NN0 ^m I ) )
699, 67fndmexd 5584 . . . . . . . . . . . . . 14 |- ( ph -> ( NN0 ^m I ) e. _V )
70 inidm 3440 . . . . . . . . . . . . . 14 |- ( ( NN0 ^m I ) i^i ( NN0 ^m I ) ) = ( NN0 ^m I )
71 eqidd 2239 . . . . . . . . . . . . . 14 |- ( ( ph /\ q e. ( NN0 ^m I ) ) -> ( X ` q ) = ( X ` q ) )
72 eqidd 2239 . . . . . . . . . . . . . 14 |- ( ( ph /\ q e. ( NN0 ^m I ) ) -> ( Y ` q ) = ( Y ` q ) )
734adantr 276 . . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. ( NN0 ^m I ) ) -> R e. Grp )
7427ffvelcdmda 5846 . . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. ( NN0 ^m I ) ) -> ( X ` q ) e. ( Base ` R ) )
7534ffvelcdmda 5846 . . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. ( NN0 ^m I ) ) -> ( Y ` q ) e. ( Base ` R ) )
7625, 57, 73, 74, 75grpcld 13878 . . . . . . . . . . . . . 14 |- ( ( ph /\ q e. ( NN0 ^m I ) ) -> ( ( X ` q ) ( +g ` R ) ( Y ` q ) ) e. ( Base ` R ) )
7767, 68, 69, 69, 70, 71, 72, 76ofvalg 6316 . . . . . . . . . . . . 13 |- ( ( ph /\ q e. ( NN0 ^m I ) ) -> ( ( X oF ( +g ` R ) Y ) ` q ) = ( ( X ` q ) ( +g ` R ) ( Y ` q ) ) )
7861, 66, 77syl2anc 415 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( ( X oF ( +g ` R ) Y ) ` q ) = ( ( X ` q ) ( +g ` R ) ( Y ` q ) ) )
7960, 78eqtrd 2271 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( ( X .+ Y ) ` q ) = ( ( X ` q ) ( +g ` R ) ( Y ` q ) ) )
80 simprr 537 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( ( X .+ Y ) ` q ) = p )
81 simprrl 545 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> a C_ c )
8281sscond 3366 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( ( NN0 ^m I ) \ c ) C_ ( ( NN0 ^m I ) \ a ) )
83 imass2 5166 . . . . . . . . . . . . . . . . 17 |- ( ( ( NN0 ^m I ) \ c ) C_ ( ( NN0 ^m I ) \ a ) -> ( X " ( ( NN0 ^m I ) \ c ) ) C_ ( X " ( ( NN0 ^m I ) \ a ) ) )
8482, 83syl 14 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( X " ( ( NN0 ^m I ) \ c ) ) C_ ( X " ( ( NN0 ^m I ) \ a ) ) )
85 simpr3 1036 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) -> ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } )
8685ad2antrr 492 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } )
8728difeq1d 3346 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( dom X \ a ) = ( ( NN0 ^m I ) \ a ) )
8887imaeq2d 5129 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( X " ( dom X \ a ) ) = ( X " ( ( NN0 ^m I ) \ a ) ) )
8988sseq1d 3277 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } <-> ( X " ( ( NN0 ^m I ) \ a ) ) C_ { ( 0g ` R ) } ) )
9089ad3antrrr 496 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } <-> ( X " ( ( NN0 ^m I ) \ a ) ) C_ { ( 0g ` R ) } ) )
9186, 90mpbid 147 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( X " ( ( NN0 ^m I ) \ a ) ) C_ { ( 0g ` R ) } )
9284, 91sstrd 3258 . . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( X " ( ( NN0 ^m I ) \ c ) ) C_ { ( 0g ` R ) } )
9392ad2antrr 492 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( X " ( ( NN0 ^m I ) \ c ) ) C_ { ( 0g ` R ) } )
9461, 67syl 14 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> X Fn ( NN0 ^m I ) )
9551difeq1d 3346 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( dom ( X .+ Y ) \ c ) = ( ( NN0 ^m I ) \ c ) )
9695eleq2d 2308 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( q e. ( dom ( X .+ Y ) \ c ) <-> q e. ( ( NN0 ^m I ) \ c ) ) )
9796ad5antr 500 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( q e. ( dom ( X .+ Y ) \ c ) <-> q e. ( ( NN0 ^m I ) \ c ) ) )
9862, 97mpbid 147 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> q e. ( ( NN0 ^m I ) \ c ) )
9994, 66, 98fnfvimad 5957 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( X ` q ) e. ( X " ( ( NN0 ^m I ) \ c ) ) )
10093, 99sseldd 3249 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( X ` q ) e. { ( 0g ` R ) } )
101 elsni 3727 . . . . . . . . . . . . 13 |- ( ( X ` q ) e. { ( 0g ` R ) } -> ( X ` q ) = ( 0g ` R ) )
102100, 101syl 14 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( X ` q ) = ( 0g ` R ) )
103 simprrr 546 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> b C_ c )
104103sscond 3366 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( ( NN0 ^m I ) \ c ) C_ ( ( NN0 ^m I ) \ b ) )
105 imass2 5166 . . . . . . . . . . . . . . . . 17 |- ( ( ( NN0 ^m I ) \ c ) C_ ( ( NN0 ^m I ) \ b ) -> ( Y " ( ( NN0 ^m I ) \ c ) ) C_ ( Y " ( ( NN0 ^m I ) \ b ) ) )
106104, 105syl 14 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( Y " ( ( NN0 ^m I ) \ c ) ) C_ ( Y " ( ( NN0 ^m I ) \ b ) ) )
107 simplr3 1072 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } )
10835difeq1d 3346 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( dom Y \ b ) = ( ( NN0 ^m I ) \ b ) )
109108imaeq2d 5129 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( Y " ( dom Y \ b ) ) = ( Y " ( ( NN0 ^m I ) \ b ) ) )
110109sseq1d 3277 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } <-> ( Y " ( ( NN0 ^m I ) \ b ) ) C_ { ( 0g ` R ) } ) )
111110ad3antrrr 496 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } <-> ( Y " ( ( NN0 ^m I ) \ b ) ) C_ { ( 0g ` R ) } ) )
112107, 111mpbid 147 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( Y " ( ( NN0 ^m I ) \ b ) ) C_ { ( 0g ` R ) } )
113106, 112sstrd 3258 . . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( Y " ( ( NN0 ^m I ) \ c ) ) C_ { ( 0g ` R ) } )
114113ad2antrr 492 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( Y " ( ( NN0 ^m I ) \ c ) ) C_ { ( 0g ` R ) } )
11561, 68syl 14 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> Y Fn ( NN0 ^m I ) )
116115, 66, 98fnfvimad 5957 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( Y ` q ) e. ( Y " ( ( NN0 ^m I ) \ c ) ) )
117114, 116sseldd 3249 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( Y ` q ) e. { ( 0g ` R ) } )
118 elsni 3727 . . . . . . . . . . . . 13 |- ( ( Y ` q ) e. { ( 0g ` R ) } -> ( Y ` q ) = ( 0g ` R ) )
119117, 118syl 14 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( Y ` q ) = ( 0g ` R ) )
120102, 119oveq12d 6106 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( ( X ` q ) ( +g ` R ) ( Y ` q ) ) = ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) )
12179, 80, 1203eqtr3d 2279 . . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> p = ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) )
12225, 57, 14, 4, 44grpridd 13898 . . . . . . . . . . . 12 |- ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
123 elsn2g 3742 . . . . . . . . . . . . 13 |- ( ( 0g ` R ) e. ( Base ` R ) -> ( ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) e. { ( 0g ` R ) } <-> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
12444, 123syl 14 . . . . . . . . . . . 12 |- ( ph -> ( ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) e. { ( 0g ` R ) } <-> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
125122, 124mpbird 167 . . . . . . . . . . 11 |- ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) e. { ( 0g ` R ) } )
12661, 125syl 14 . . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) e. { ( 0g ` R ) } )
127121, 126eqeltrd 2315 . . . . . . . . 9 |- ( ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) /\ ( q e. ( dom ( X .+ Y ) \ c ) /\ ( ( X .+ Y ) ` q ) = p ) ) -> p e. { ( 0g ` R ) } )
12856, 127rexlimddv 2673 . . . . . . . 8 |- ( ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) /\ p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) ) -> p e. { ( 0g ` R ) } )
129128ex 115 . . . . . . 7 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( p e. ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) -> p e. { ( 0g ` R ) } ) )
130129ssrdv 3254 . . . . . 6 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( ( X .+ Y ) " ( dom ( X .+ Y ) \ c ) ) C_ { ( 0g ` R ) } )
13142, 45, 48, 49, 54, 130isfsuppfid 7297 . . . . 5 |- ( ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) /\ ( ( c C_ ( NN0 ^m I ) /\ c e. Fin ) /\ ( a C_ c /\ b C_ c ) ) ) -> ( X .+ Y ) finSupp ( 0g ` R ) )
13241, 131exlimddv 1954 . . . 4 |- ( ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) /\ ( b e. Fin /\ b C_ dom Y /\ ( Y " ( dom Y \ b ) ) C_ { ( 0g ` R ) } ) ) -> ( X .+ Y ) finSupp ( 0g ` R ) )
13323, 132exlimddv 1954 . . 3 |- ( ( ph /\ ( a e. Fin /\ a C_ dom X /\ ( X " ( dom X \ a ) ) C_ { ( 0g ` R ) } ) ) -> ( X .+ Y ) finSupp ( 0g ` R ) )
13418, 133exlimddv 1954 . 2 |- ( ph -> ( X .+ Y ) finSupp ( 0g ` R ) )
1356, 1, 2, 14, 7mplelbas 15236 . 2 |- ( ( X .+ Y ) e. U <-> ( ( X .+ Y ) e. ( Base ` S ) /\ ( X .+ Y ) finSupp ( 0g ` R ) ) )
13613, 134, 135sylanbrc 421 1 |- ( ph -> ( X .+ Y ) e. U )
Colors of variables:    wff set class
This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009   = wceq 1402   E.wex 1545   e. wcel 2209   E.wrex 2529   _Vcvv 2821   \ cdif 3217   C_ wss 3220   {csn 3709   class class class wbr 4131   dom cdm 4776   "cima 4779   Fun wfun 5374   Fn wfn 5375   ` cfv 5380  (class class class)co 6088   oFcof 6303   ^m cmap 6927   Fincfn 7028   finSupp cfsupp 7292   NN0cn0 9575   Basecbs 13410   +g cplusg 13490   0gc0g 13669   Grpcgrp 13864   mPwSer cmps 15154   mPoly cmpl 15156
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-mulrcl 8285  ax-addcom 8286  ax-mulcom 8287  ax-addass 8288  ax-mulass 8289  ax-distr 8290  ax-i2m1 8291  ax-0lt1 8292  ax-1rid 8293  ax-0id 8294  ax-rnegex 8295  ax-precex 8296  ax-cnre 8297  ax-pre-ltirr 8298  ax-pre-ltwlin 8299  ax-pre-lttrn 8300  ax-pre-apti 8301  ax-pre-ltadd 8302  ax-pre-mulgt0 8303  ax-pre-mulext 8304  ax-arch 8305  ax-caucvg 8306
This proof depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-tp 3717  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-po 4443  df-iso 4444  df-iord 4513  df-on 4515  df-ilim 4516  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-of 6305  df-ofr 6306  df-1st 6378  df-2nd 6379  df-recs 6581  df-frec 6667  df-1o 6692  df-er 6812  df-map 6929  df-ixp 6987  df-en 7029  df-fin 7031  df-fsuppfi 7293  df-sup 7331  df-pnf 8369  df-mnf 8370  df-xr 8371  df-ltxr 8372  df-le 8373  df-sub 8507  df-neg 8508  df-reap 8912  df-ap 8919  df-div 9012  df-inn 9315  df-2 9373  df-3 9374  df-4 9375  df-5 9376  df-6 9377  df-7 9378  df-8 9379  df-9 9380  df-n0 9576  df-z 9655  df-uz 9938  df-rp 10072  df-fz 10429  df-seqfrec 10906  df-exp 10997  df-cj 11629  df-re 11630  df-im 11631  df-rsqrt 11786  df-abs 11787  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13416  df-sets 13417  df-iress 13418  df-plusg 13503  df-mulr 13504  df-sca 13506  df-vsca 13507  df-tset 13509  df-rest 13654  df-topn 13655  df-0g 13671  df-topgen 13673  df-pt 13674  df-mgm 13735  df-sgrp 13776  df-mnd 13789  df-grp 13867  df-psr 15157  df-mpl 15159
This theorem is used by:  mplsubgfi  15248
  Copyright terms: Public domain W3C validator