Metamath Proof Explorer


Theorem psdmul

Description: Product rule for power series. An outline is available at https://github.com/icecream17/Stuff/blob/main/math/psdmul.pdf . (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses psdmul.s S = I mPwSer R
psdmul.b B = Base S
psdmul.p + ˙ = + S
psdmul.m · ˙ = S
psdmul.r φ R CRing
psdmul.x φ X I
psdmul.f φ F B
psdmul.g φ G B
Assertion psdmul φ I mPSDer R X F · ˙ G = I mPSDer R X F · ˙ G + ˙ F · ˙ I mPSDer R X G

Proof

Step Hyp Ref Expression
1 psdmul.s S = I mPwSer R
2 psdmul.b B = Base S
3 psdmul.p + ˙ = + S
4 psdmul.m · ˙ = S
5 psdmul.r φ R CRing
6 psdmul.x φ X I
7 psdmul.f φ F B
8 psdmul.g φ G B
9 eqid Base R = Base R
10 eqid + R = + R
11 5 crngringd φ R Ring
12 11 ringcmnd φ R CMnd
13 12 adantr φ d h 0 I | h -1 Fin R CMnd
14 simpr φ d h 0 I | h -1 Fin d h 0 I | h -1 Fin
15 reldmpsr Rel dom mPwSer
16 1 2 15 strov2rcl F B I V
17 7 16 syl φ I V
18 eqid h 0 I | h -1 Fin = h 0 I | h -1 Fin
19 18 psrbagsn I V y I if y = X 1 0 h 0 I | h -1 Fin
20 17 19 syl φ y I if y = X 1 0 h 0 I | h -1 Fin
21 20 adantr φ d h 0 I | h -1 Fin y I if y = X 1 0 h 0 I | h -1 Fin
22 18 psrbagaddcl d h 0 I | h -1 Fin y I if y = X 1 0 h 0 I | h -1 Fin d + f y I if y = X 1 0 h 0 I | h -1 Fin
23 14 21 22 syl2anc φ d h 0 I | h -1 Fin d + f y I if y = X 1 0 h 0 I | h -1 Fin
24 18 psrbaglefi d + f y I if y = X 1 0 h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 Fin
25 23 24 syl φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 Fin
26 eqid R = R
27 5 crnggrpd φ R Grp
28 27 grpmndd φ R Mnd
29 28 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 R Mnd
30 18 psrbagf d h 0 I | h -1 Fin d : I 0
31 30 adantl φ d h 0 I | h -1 Fin d : I 0
32 6 adantr φ d h 0 I | h -1 Fin X I
33 31 32 ffvelcdmd φ d h 0 I | h -1 Fin d X 0
34 peano2nn0 d X 0 d X + 1 0
35 33 34 syl φ d h 0 I | h -1 Fin d X + 1 0
36 35 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d X + 1 0
37 eqid R = R
38 11 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 R Ring
39 1 9 18 2 7 psrelbas φ F : h 0 I | h -1 Fin Base R
40 39 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F : h 0 I | h -1 Fin Base R
41 elrabi u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u h 0 I | h -1 Fin
42 41 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u h 0 I | h -1 Fin
43 40 42 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u Base R
44 1 9 18 2 8 psrelbas φ G : h 0 I | h -1 Fin Base R
45 44 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 G : h 0 I | h -1 Fin Base R
46 eqid k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
47 18 46 psrbagconcl d + f y I if y = X 1 0 h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d + f y I if y = X 1 0 f u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
48 23 47 sylan φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d + f y I if y = X 1 0 f u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
49 elrabi d + f y I if y = X 1 0 f u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d + f y I if y = X 1 0 f u h 0 I | h -1 Fin
50 48 49 syl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d + f y I if y = X 1 0 f u h 0 I | h -1 Fin
51 45 50 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 G d + f y I if y = X 1 0 f u Base R
52 9 37 38 43 51 ringcld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u Base R
53 9 26 29 36 52 mulgnn0cld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
54 disjdifr k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d =
55 54 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d =
56 1nn0 1 0
57 0nn0 0 0
58 56 57 ifcli if i = X 1 0 0
59 58 nn0ge0i 0 if i = X 1 0
60 31 ffvelcdmda φ d h 0 I | h -1 Fin i I d i 0
61 60 nn0red φ d h 0 I | h -1 Fin i I d i
62 58 nn0rei if i = X 1 0
63 62 a1i φ d h 0 I | h -1 Fin i I if i = X 1 0
64 61 63 addge01d φ d h 0 I | h -1 Fin i I 0 if i = X 1 0 d i d i + if i = X 1 0
65 59 64 mpbii φ d h 0 I | h -1 Fin i I d i d i + if i = X 1 0
66 65 ralrimiva φ d h 0 I | h -1 Fin i I d i d i + if i = X 1 0
67 31 ffnd φ d h 0 I | h -1 Fin d Fn I
68 56 57 ifcli if y = X 1 0 0
69 68 elexi if y = X 1 0 V
70 eqid y I if y = X 1 0 = y I if y = X 1 0
71 69 70 fnmpti y I if y = X 1 0 Fn I
72 71 a1i φ d h 0 I | h -1 Fin y I if y = X 1 0 Fn I
73 17 adantr φ d h 0 I | h -1 Fin I V
74 inidm I I = I
75 67 72 73 73 74 offn φ d h 0 I | h -1 Fin d + f y I if y = X 1 0 Fn I
76 eqidd φ d h 0 I | h -1 Fin i I d i = d i
77 eqeq1 y = i y = X i = X
78 77 ifbid y = i if y = X 1 0 = if i = X 1 0
79 58 elexi if i = X 1 0 V
80 78 70 79 fvmpt i I y I if y = X 1 0 i = if i = X 1 0
81 80 adantl φ d h 0 I | h -1 Fin i I y I if y = X 1 0 i = if i = X 1 0
82 67 72 73 73 74 76 81 ofval φ d h 0 I | h -1 Fin i I d + f y I if y = X 1 0 i = d i + if i = X 1 0
83 67 75 73 73 74 76 82 ofrfval φ d h 0 I | h -1 Fin d f d + f y I if y = X 1 0 i I d i d i + if i = X 1 0
84 66 83 mpbird φ d h 0 I | h -1 Fin d f d + f y I if y = X 1 0
85 84 adantr φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin d f d + f y I if y = X 1 0
86 17 ad2antrr φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin I V
87 18 psrbagf k h 0 I | h -1 Fin k : I 0
88 87 adantl φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin k : I 0
89 31 adantr φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin d : I 0
90 18 psrbagf d + f y I if y = X 1 0 h 0 I | h -1 Fin d + f y I if y = X 1 0 : I 0
91 23 90 syl φ d h 0 I | h -1 Fin d + f y I if y = X 1 0 : I 0
92 91 adantr φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin d + f y I if y = X 1 0 : I 0
93 nn0re q 0 q
94 nn0re r 0 r
95 nn0re s 0 s
96 letr q r s q r r s q s
97 93 94 95 96 syl3an q 0 r 0 s 0 q r r s q s
98 97 adantl φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin q 0 r 0 s 0 q r r s q s
99 86 88 89 92 98 caoftrn φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin k f d d f d + f y I if y = X 1 0 k f d + f y I if y = X 1 0
100 85 99 mpan2d φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin k f d k f d + f y I if y = X 1 0
101 100 ss2rabdv φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
102 undifr k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
103 101 102 sylib φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
104 103 eqcomd φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d
105 9 10 13 25 53 55 104 gsummptfidmsplit φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u
106 eqid 0 R = 0 R
107 ovex 0 I V
108 107 rabex h 0 I | h -1 Fin V
109 108 rabex k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 V
110 109 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 V
111 ovex F u R G d + f y I if y = X 1 0 f u V
112 eqid u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u
113 111 112 fnmpti u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
114 113 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
115 fvexd φ d h 0 I | h -1 Fin 0 R V
116 114 25 115 fndmfifsupp φ d h 0 I | h -1 Fin finSupp 0 R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u
117 9 106 26 110 52 116 13 35 gsummulg φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = d X + 1 R R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u
118 difrab k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d
119 118 eleq2i u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d
120 breq1 k = u k f d + f y I if y = X 1 0 u f d + f y I if y = X 1 0
121 breq1 k = u k f d u f d
122 121 notbid k = u ¬ k f d ¬ u f d
123 120 122 anbi12d k = u k f d + f y I if y = X 1 0 ¬ k f d u f d + f y I if y = X 1 0 ¬ u f d
124 123 elrab u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d u h 0 I | h -1 Fin u f d + f y I if y = X 1 0 ¬ u f d
125 18 psrbagf u h 0 I | h -1 Fin u : I 0
126 125 ffnd u h 0 I | h -1 Fin u Fn I
127 126 adantl φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u Fn I
128 75 adantr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin d + f y I if y = X 1 0 Fn I
129 17 ad2antrr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin I V
130 eqidd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i = u i
131 67 adantr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin d Fn I
132 68 a1i y I if y = X 1 0 0
133 70 132 fmpti y I if y = X 1 0 : I 0
134 133 a1i φ y I if y = X 1 0 : I 0
135 134 ffnd φ y I if y = X 1 0 Fn I
136 135 ad2antrr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin y I if y = X 1 0 Fn I
137 eqidd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I d i = d i
138 80 adantl φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I y I if y = X 1 0 i = if i = X 1 0
139 131 136 129 129 74 137 138 ofval φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I d + f y I if y = X 1 0 i = d i + if i = X 1 0
140 127 128 129 129 74 130 139 ofrfval φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u f d + f y I if y = X 1 0 i I u i d i + if i = X 1 0
141 127 131 129 129 74 130 137 ofrfval φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u f d i I u i d i
142 141 notbid φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin ¬ u f d ¬ i I u i d i
143 rexnal i I ¬ u i d i ¬ i I u i d i
144 142 143 bitr4di φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin ¬ u f d i I ¬ u i d i
145 140 144 anbi12d φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u f d + f y I if y = X 1 0 ¬ u f d i I u i d i + if i = X 1 0 i I ¬ u i d i
146 33 ad2antrr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i d X 0
147 125 adantl φ u h 0 I | h -1 Fin u : I 0
148 6 adantr φ u h 0 I | h -1 Fin X I
149 147 148 ffvelcdmd φ u h 0 I | h -1 Fin u X 0
150 149 adantlr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u X 0
151 150 adantr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i u X 0
152 nn0nlt0 d X 0 ¬ d X < 0
153 146 152 syl φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i ¬ d X < 0
154 31 adantr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin d : I 0
155 154 ffvelcdmda φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I d i 0
156 155 nn0cnd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I d i
157 156 addridd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I d i + 0 = d i
158 157 breq2d φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + 0 u i d i
159 158 biimpd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + 0 u i d i
160 ifnefalse i X if i = X 1 0 = 0
161 160 oveq2d i X d i + if i = X 1 0 = d i + 0
162 161 breq2d i X u i d i + if i = X 1 0 u i d i + 0
163 162 imbi1d i X u i d i + if i = X 1 0 u i d i u i d i + 0 u i d i
164 159 163 syl5ibrcom φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I i X u i d i + if i = X 1 0 u i d i
165 164 imp φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I i X u i d i + if i = X 1 0 u i d i
166 165 impancom φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i X u i d i
167 166 necon1bd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 ¬ u i d i i = X
168 167 ancrd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 ¬ u i d i i = X ¬ u i d i
169 168 ex φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 ¬ u i d i i = X ¬ u i d i
170 169 ralimdva φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i i = X ¬ u i d i
171 170 anim1d φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i i I ¬ u i d i i = X ¬ u i d i i I ¬ u i d i
172 171 imp φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i i I ¬ u i d i i = X ¬ u i d i i I ¬ u i d i
173 rexim i I ¬ u i d i i = X ¬ u i d i i I ¬ u i d i i I i = X ¬ u i d i
174 173 imp i I ¬ u i d i i = X ¬ u i d i i I ¬ u i d i i I i = X ¬ u i d i
175 fveq2 i = X u i = u X
176 fveq2 i = X d i = d X
177 175 176 breq12d i = X u i d i u X d X
178 177 notbid i = X ¬ u i d i ¬ u X d X
179 178 ceqsrexbv i I i = X ¬ u i d i X I ¬ u X d X
180 179 simprbi i I i = X ¬ u i d i ¬ u X d X
181 174 180 syl i I ¬ u i d i i = X ¬ u i d i i I ¬ u i d i ¬ u X d X
182 33 adantr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin d X 0
183 182 nn0red φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin d X
184 150 nn0red φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u X
185 183 184 ltnled φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin d X < u X ¬ u X d X
186 185 biimpar φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin ¬ u X d X d X < u X
187 181 186 sylan2 φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I ¬ u i d i i = X ¬ u i d i i I ¬ u i d i d X < u X
188 172 187 syldan φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i d X < u X
189 breq2 u X = 0 d X < u X d X < 0
190 188 189 syl5ibcom φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i u X = 0 d X < 0
191 153 190 mtod φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i ¬ u X = 0
192 191 neqned φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i u X 0
193 elnnne0 u X u X 0 u X 0
194 151 192 193 sylanbrc φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i u X
195 elfzo0 d X 0 ..^ u X d X 0 u X d X < u X
196 146 194 188 195 syl3anbrc φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i d X 0 ..^ u X
197 fzostep1 d X 0 ..^ u X d X + 1 0 ..^ u X d X + 1 = u X
198 196 197 syl φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i d X + 1 0 ..^ u X d X + 1 = u X
199 151 nn0red φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i u X
200 35 ad2antrr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i d X + 1 0
201 200 nn0red φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i d X + 1
202 6 ad2antrr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin X I
203 iftrue i = X if i = X 1 0 = 1
204 176 203 oveq12d i = X d i + if i = X 1 0 = d X + 1
205 175 204 breq12d i = X u i d i + if i = X 1 0 u X d X + 1
206 205 rspcv X I i I u i d i + if i = X 1 0 u X d X + 1
207 202 206 syl φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 u X d X + 1
208 207 imp φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 u X d X + 1
209 208 adantrr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i u X d X + 1
210 199 201 209 lensymd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i ¬ d X + 1 < u X
211 210 intn3an3d φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i ¬ d X + 1 0 u X d X + 1 < u X
212 elfzo0 d X + 1 0 ..^ u X d X + 1 0 u X d X + 1 < u X
213 211 212 sylnibr φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i ¬ d X + 1 0 ..^ u X
214 198 213 orcnd φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin i I u i d i + if i = X 1 0 i I ¬ u i d i d X + 1 = u X
215 145 214 sylbida φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u f d + f y I if y = X 1 0 ¬ u f d d X + 1 = u X
216 215 anasss φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin u f d + f y I if y = X 1 0 ¬ u f d d X + 1 = u X
217 124 216 sylan2b φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d d X + 1 = u X
218 119 217 sylan2b φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d d X + 1 = u X
219 218 oveq1d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u = u X R F u R G d + f y I if y = X 1 0 f u
220 219 mpteq2dva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u
221 220 oveq2d φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u
222 18 psrbaglefi d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d Fin
223 222 adantl φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d Fin
224 28 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d R Mnd
225 35 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d X + 1 0
226 11 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d R Ring
227 elrabi u k h 0 I | h -1 Fin | k f d u h 0 I | h -1 Fin
228 39 adantr φ d h 0 I | h -1 Fin F : h 0 I | h -1 Fin Base R
229 228 ffvelcdmda φ d h 0 I | h -1 Fin u h 0 I | h -1 Fin F u Base R
230 227 229 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d F u Base R
231 44 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d G : h 0 I | h -1 Fin Base R
232 31 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d : I 0
233 232 ffvelcdmda φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d i 0
234 233 nn0cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d i
235 227 125 syl u k h 0 I | h -1 Fin | k f d u : I 0
236 235 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d u : I 0
237 236 ffvelcdmda φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I u i 0
238 237 nn0cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I u i
239 58 nn0cni if i = X 1 0
240 239 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I if i = X 1 0
241 234 238 240 subadd23d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d i - u i + if i = X 1 0 = d i + if i = X 1 0 - u i
242 234 240 238 addsubassd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d i + if i = X 1 0 - u i = d i + if i = X 1 0 - u i
243 241 242 eqtr4d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d i - u i + if i = X 1 0 = d i + if i = X 1 0 - u i
244 243 mpteq2dva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d i - u i + if i = X 1 0 = i I d i + if i = X 1 0 - u i
245 eqid k h 0 I | h -1 Fin | k f d = k h 0 I | h -1 Fin | k f d
246 18 245 psrbagconcl d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u k h 0 I | h -1 Fin | k f d
247 elrabi d f u k h 0 I | h -1 Fin | k f d d f u h 0 I | h -1 Fin
248 246 247 syl d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u h 0 I | h -1 Fin
249 248 adantll φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u h 0 I | h -1 Fin
250 18 psrbagf d f u h 0 I | h -1 Fin d f u : I 0
251 249 250 syl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u : I 0
252 251 ffnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u Fn I
253 71 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d y I if y = X 1 0 Fn I
254 17 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d I V
255 232 ffnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d Fn I
256 236 ffnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d u Fn I
257 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d i = d i
258 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I u i = u i
259 255 256 254 254 74 257 258 ofval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d f u i = d i u i
260 80 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I y I if y = X 1 0 i = if i = X 1 0
261 252 253 254 254 74 259 260 offval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u + f y I if y = X 1 0 = i I d i - u i + if i = X 1 0
262 simplr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d h 0 I | h -1 Fin
263 20 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d y I if y = X 1 0 h 0 I | h -1 Fin
264 262 263 22 syl2anc φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d + f y I if y = X 1 0 h 0 I | h -1 Fin
265 264 90 syl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d + f y I if y = X 1 0 : I 0
266 265 ffnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d + f y I if y = X 1 0 Fn I
267 255 253 254 254 74 257 260 ofval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d i I d + f y I if y = X 1 0 i = d i + if i = X 1 0
268 266 256 254 254 74 267 258 offval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d + f y I if y = X 1 0 f u = i I d i + if i = X 1 0 - u i
269 244 261 268 3eqtr4d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u + f y I if y = X 1 0 = d + f y I if y = X 1 0 f u
270 18 psrbagaddcl d f u h 0 I | h -1 Fin y I if y = X 1 0 h 0 I | h -1 Fin d f u + f y I if y = X 1 0 h 0 I | h -1 Fin
271 249 263 270 syl2anc φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u + f y I if y = X 1 0 h 0 I | h -1 Fin
272 269 271 eqeltrrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d + f y I if y = X 1 0 f u h 0 I | h -1 Fin
273 231 272 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d G d + f y I if y = X 1 0 f u Base R
274 9 37 226 230 273 ringcld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d F u R G d + f y I if y = X 1 0 f u Base R
275 9 26 224 225 274 mulgnn0cld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
276 disjdifr k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d k X = 0 =
277 276 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d k X = 0 =
278 simpl k f d k X = 0 k f d
279 278 a1i k h 0 I | h -1 Fin k f d k X = 0 k f d
280 279 ss2rabi k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d
281 280 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d
282 undifr k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d k X = 0 = k h 0 I | h -1 Fin | k f d
283 281 282 sylib φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d k X = 0 = k h 0 I | h -1 Fin | k f d
284 283 eqcomd φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d = k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d k X = 0
285 9 10 13 223 275 277 284 gsummptfidmsplit φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u
286 eldifi u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u k h 0 I | h -1 Fin | k f d
287 6 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d X I
288 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d X I d X = d X
289 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d X I u X = u X
290 255 256 254 254 74 288 289 ofval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d X I d f u X = d X u X
291 287 290 mpdan φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u X = d X u X
292 286 291 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X = d X u X
293 292 oveq2d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X + d f u X = u X + d X - u X
294 236 287 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d u X 0
295 286 294 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X 0
296 295 nn0cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X
297 33 nn0cnd φ d h 0 I | h -1 Fin d X
298 297 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X
299 296 298 pncan3d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X + d X - u X = d X
300 293 299 eqtrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X + d f u X = d X
301 300 oveq1d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X + d f u X + 1 = d X + 1
302 251 287 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u X 0
303 286 302 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X 0
304 303 nn0cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X
305 1cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 1
306 296 304 305 addassd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X + d f u X + 1 = u X + d f u X + 1
307 301 306 eqtr3d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 = u X + d f u X + 1
308 307 oveq1d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = u X + d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
309 28 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 R Mnd
310 peano2nn0 d f u X 0 d f u X + 1 0
311 302 310 syl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u X + 1 0
312 286 311 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 0
313 286 274 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 F u R G d + f y I if y = X 1 0 f u Base R
314 9 26 10 mulgnn0dir R Mnd u X 0 d f u X + 1 0 F u R G d + f y I if y = X 1 0 f u Base R u X + d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = u X R F u R G d + f y I if y = X 1 0 f u + R d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
315 309 295 312 313 314 syl13anc φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X + d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = u X R F u R G d + f y I if y = X 1 0 f u + R d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
316 308 315 eqtrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = u X R F u R G d + f y I if y = X 1 0 f u + R d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
317 316 mpteq2dva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
318 317 oveq2d φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
319 difssd φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d
320 223 319 ssfid φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 Fin
321 9 26 224 294 274 mulgnn0cld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u Base R
322 286 321 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u Base R
323 9 26 224 311 274 mulgnn0cld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
324 286 323 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
325 eqid u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u
326 eqid u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
327 9 10 13 320 322 324 325 326 gsummptfidmadd φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
328 318 327 eqtrd φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
329 6 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 X I
330 67 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d Fn I
331 elrabi u k h 0 I | h -1 Fin | k f d k X = 0 u h 0 I | h -1 Fin
332 331 126 syl u k h 0 I | h -1 Fin | k f d k X = 0 u Fn I
333 332 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 u Fn I
334 17 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 I V
335 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 X I d X = d X
336 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 X I u X = u X
337 330 333 334 334 74 335 336 ofval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 X I d f u X = d X u X
338 329 337 mpdan φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d f u X = d X u X
339 fveq1 k = u k X = u X
340 339 eqeq1d k = u k X = 0 u X = 0
341 121 340 anbi12d k = u k f d k X = 0 u f d u X = 0
342 341 elrab u k h 0 I | h -1 Fin | k f d k X = 0 u h 0 I | h -1 Fin u f d u X = 0
343 342 simprbi u k h 0 I | h -1 Fin | k f d k X = 0 u f d u X = 0
344 343 simprd u k h 0 I | h -1 Fin | k f d k X = 0 u X = 0
345 344 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 u X = 0
346 345 oveq2d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X u X = d X 0
347 33 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X 0
348 347 nn0cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X
349 348 subid1d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X 0 = d X
350 338 346 349 3eqtrrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X = d f u X
351 350 oveq1d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 = d f u X + 1
352 351 oveq1d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
353 352 mpteq2dva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
354 353 oveq2d φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
355 328 354 oveq12d φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
356 27 adantr φ d h 0 I | h -1 Fin R Grp
357 108 rabex k h 0 I | h -1 Fin | k f d V
358 357 difexi k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 V
359 358 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 V
360 322 fmpttd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u : k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 Base R
361 ovex u X R F u R G d + f y I if y = X 1 0 f u V
362 361 325 fnmpti u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0
363 362 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0
364 363 320 115 fndmfifsupp φ d h 0 I | h -1 Fin finSupp 0 R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u
365 9 106 13 359 360 364 gsumcl φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u Base R
366 324 fmpttd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u : k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 Base R
367 ovex d f u X + 1 R F u R G d + f y I if y = X 1 0 f u V
368 367 326 fnmpti u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0
369 368 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0
370 369 320 115 fndmfifsupp φ d h 0 I | h -1 Fin finSupp 0 R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
371 9 106 13 359 366 370 gsumcl φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
372 108 rabex k h 0 I | h -1 Fin | k f d k X = 0 V
373 372 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k X = 0 V
374 280 sseli u k h 0 I | h -1 Fin | k f d k X = 0 u k h 0 I | h -1 Fin | k f d
375 374 323 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
376 375 fmpttd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u : k h 0 I | h -1 Fin | k f d k X = 0 Base R
377 eqid u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
378 367 377 fnmpti u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d k X = 0
379 378 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d k X = 0
380 223 281 ssfid φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d k X = 0 Fin
381 379 380 115 fndmfifsupp φ d h 0 I | h -1 Fin finSupp 0 R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
382 9 106 13 373 376 381 gsumcl φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
383 9 10 356 365 371 382 grpassd φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
384 285 355 383 3eqtrd φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
385 221 384 oveq12d φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d d X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
386 105 117 385 3eqtr3d φ d h 0 I | h -1 Fin d X + 1 R R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
387 7 adantr φ d h 0 I | h -1 Fin F B
388 8 adantr φ d h 0 I | h -1 Fin G B
389 1 2 37 4 18 387 388 23 psrmulval φ d h 0 I | h -1 Fin F · ˙ G d + f y I if y = X 1 0 = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u
390 389 oveq2d φ d h 0 I | h -1 Fin d X + 1 R F · ˙ G d + f y I if y = X 1 0 = d X + 1 R R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u
391 109 difexi k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d V
392 391 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d V
393 eldifi u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
394 41 125 syl u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u : I 0
395 394 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u : I 0
396 6 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 X I
397 395 396 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u X 0
398 9 26 29 397 52 mulgnn0cld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u Base R
399 393 398 sylan2 φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u Base R
400 399 fmpttd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u : k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d Base R
401 eqid u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u
402 361 401 fnmpti u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
403 402 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
404 difssd φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
405 25 404 ssfid φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d Fin
406 403 405 115 fndmfifsupp φ d h 0 I | h -1 Fin finSupp 0 R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u
407 9 106 13 392 400 406 gsumcl φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u Base R
408 9 10 356 371 382 grpcld φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u Base R
409 9 10 356 407 365 408 grpassd φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
410 386 390 409 3eqtr4d φ d h 0 I | h -1 Fin d X + 1 R F · ˙ G d + f y I if y = X 1 0 = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
411 410 mpteq2dva φ d h 0 I | h -1 Fin d X + 1 R F · ˙ G d + f y I if y = X 1 0 = d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
412 1 2 4 11 7 8 psrmulcl φ F · ˙ G B
413 1 2 18 6 412 psdval φ I mPSDer R X F · ˙ G = d h 0 I | h -1 Fin d X + 1 R F · ˙ G d + f y I if y = X 1 0
414 27 grpmgmd φ R Mgm
415 1 2 414 6 7 psdcl φ I mPSDer R X F B
416 1 2 4 11 415 8 psrmulcl φ I mPSDer R X F · ˙ G B
417 1 2 414 6 8 psdcl φ I mPSDer R X G B
418 1 2 4 11 7 417 psrmulcl φ F · ˙ I mPSDer R X G B
419 1 2 10 3 416 418 psradd φ I mPSDer R X F · ˙ G + ˙ F · ˙ I mPSDer R X G = I mPSDer R X F · ˙ G + R f F · ˙ I mPSDer R X G
420 1 9 18 2 416 psrelbas φ I mPSDer R X F · ˙ G : h 0 I | h -1 Fin Base R
421 420 ffnd φ I mPSDer R X F · ˙ G Fn h 0 I | h -1 Fin
422 1 9 18 2 418 psrelbas φ F · ˙ I mPSDer R X G : h 0 I | h -1 Fin Base R
423 422 ffnd φ F · ˙ I mPSDer R X G Fn h 0 I | h -1 Fin
424 108 a1i φ h 0 I | h -1 Fin V
425 inidm h 0 I | h -1 Fin h 0 I | h -1 Fin = h 0 I | h -1 Fin
426 415 adantr φ d h 0 I | h -1 Fin I mPSDer R X F B
427 1 2 37 4 18 426 388 14 psrmulval φ d h 0 I | h -1 Fin I mPSDer R X F · ˙ G d = R b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b
428 357 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d V
429 11 ad2antrr φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d R Ring
430 elrabi b k h 0 I | h -1 Fin | k f d b h 0 I | h -1 Fin
431 1 9 18 2 415 psrelbas φ I mPSDer R X F : h 0 I | h -1 Fin Base R
432 431 adantr φ d h 0 I | h -1 Fin I mPSDer R X F : h 0 I | h -1 Fin Base R
433 432 ffvelcdmda φ d h 0 I | h -1 Fin b h 0 I | h -1 Fin I mPSDer R X F b Base R
434 430 433 sylan2 φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d I mPSDer R X F b Base R
435 44 ad2antrr φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d G : h 0 I | h -1 Fin Base R
436 18 245 psrbagconcl d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d d f b k h 0 I | h -1 Fin | k f d
437 436 adantll φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d d f b k h 0 I | h -1 Fin | k f d
438 elrabi d f b k h 0 I | h -1 Fin | k f d d f b h 0 I | h -1 Fin
439 437 438 syl φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d d f b h 0 I | h -1 Fin
440 435 439 ffvelcdmd φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d G d f b Base R
441 9 37 429 434 440 ringcld φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b Base R
442 441 fmpttd φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b : k h 0 I | h -1 Fin | k f d Base R
443 ovex I mPSDer R X F b R G d f b V
444 eqid b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b = b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b
445 443 444 fnmpti b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b Fn k h 0 I | h -1 Fin | k f d
446 445 a1i φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b Fn k h 0 I | h -1 Fin | k f d
447 446 223 115 fndmfifsupp φ d h 0 I | h -1 Fin finSupp 0 R b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b
448 eqid u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 = u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0
449 df-of f + = m V , n V o dom m dom n m o + n o
450 vex u V
451 450 a1i φ d h 0 I | h -1 Fin u V
452 ssv k h 0 I | h -1 Fin | k f d V
453 452 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d V
454 ssv y I if y = X 1 0 V
455 454 a1i φ d h 0 I | h -1 Fin y I if y = X 1 0 V
456 449 451 453 455 elimampo φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o
457 456 biimpa φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o
458 elrabi m k h 0 I | h -1 Fin | k f d m h 0 I | h -1 Fin
459 18 psrbagf m h 0 I | h -1 Fin m : I 0
460 459 ffund m h 0 I | h -1 Fin Fun m
461 458 460 syl m k h 0 I | h -1 Fin | k f d Fun m
462 461 funfnd m k h 0 I | h -1 Fin | k f d m Fn dom m
463 462 ad2antrl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 m Fn dom m
464 velsn n y I if y = X 1 0 n = y I if y = X 1 0
465 funmpt Fun y I if y = X 1 0
466 funeq n = y I if y = X 1 0 Fun n Fun y I if y = X 1 0
467 465 466 mpbiri n = y I if y = X 1 0 Fun n
468 467 funfnd n = y I if y = X 1 0 n Fn dom n
469 464 468 sylbi n y I if y = X 1 0 n Fn dom n
470 469 ad2antll φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 n Fn dom n
471 vex m V
472 471 dmex dom m V
473 472 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 dom m V
474 vex n V
475 474 dmex dom n V
476 475 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 dom n V
477 eqid dom m dom n = dom m dom n
478 eqidd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 o dom m m o = m o
479 eqidd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 o dom n n o = n o
480 463 470 473 476 477 478 479 offval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 m + f n = o dom m dom n m o + n o
481 480 eqeq2d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u = o dom m dom n m o + n o
482 elsni n y I if y = X 1 0 n = y I if y = X 1 0
483 482 oveq2d n y I if y = X 1 0 m + f n = m + f y I if y = X 1 0
484 483 eqeq2d n y I if y = X 1 0 u = m + f n u = m + f y I if y = X 1 0
485 484 ad2antll φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u = m + f y I if y = X 1 0
486 17 ad3antrrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d I V
487 458 459 syl m k h 0 I | h -1 Fin | k f d m : I 0
488 487 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m : I 0
489 133 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d y I if y = X 1 0 : I 0
490 nn0cn q 0 q
491 nn0cn r 0 r
492 nn0cn s 0 s
493 addsubass q r s q + r - s = q + r - s
494 490 491 492 493 syl3an q 0 r 0 s 0 q + r - s = q + r - s
495 494 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d q 0 r 0 s 0 q + r - s = q + r - s
496 486 488 489 489 495 caofass φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f y I if y = X 1 0 = m + f y I if y = X 1 0 f y I if y = X 1 0
497 simpr φ i I i I
498 58 a1i φ i I if i = X 1 0 0
499 70 78 497 498 fvmptd3 φ i I y I if y = X 1 0 i = if i = X 1 0
500 135 135 17 17 74 499 499 offval φ y I if y = X 1 0 f y I if y = X 1 0 = i I if i = X 1 0 if i = X 1 0
501 500 oveq2d φ m + f y I if y = X 1 0 f y I if y = X 1 0 = m + f i I if i = X 1 0 if i = X 1 0
502 501 ad3antrrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f y I if y = X 1 0 = m + f i I if i = X 1 0 if i = X 1 0
503 239 subidi if i = X 1 0 if i = X 1 0 = 0
504 503 mpteq2i i I if i = X 1 0 if i = X 1 0 = i I 0
505 fconstmpt I × 0 = i I 0
506 504 505 eqtr4i i I if i = X 1 0 if i = X 1 0 = I × 0
507 506 oveq2i m + f i I if i = X 1 0 if i = X 1 0 = m + f I × 0
508 0zd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d 0
509 490 addridd q 0 q + 0 = q
510 509 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d q 0 q + 0 = q
511 486 488 508 510 caofid0r φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f I × 0 = m
512 507 511 eqtrid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f i I if i = X 1 0 if i = X 1 0 = m
513 496 502 512 3eqtrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f y I if y = X 1 0 = m
514 simpr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m k h 0 I | h -1 Fin | k f d
515 513 514 eqeltrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
516 oveq1 u = m + f y I if y = X 1 0 u f y I if y = X 1 0 = m + f y I if y = X 1 0 f y I if y = X 1 0
517 516 eleq1d u = m + f y I if y = X 1 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
518 515 517 syl5ibrcom φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d u = m + f y I if y = X 1 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
519 518 adantrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f y I if y = X 1 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
520 485 519 sylbid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
521 481 520 sylbird φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
522 521 rexlimdvva φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
523 457 522 mpd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
524 simpr φ d h 0 I | h -1 Fin v k h 0 I | h -1 Fin | k f d v k h 0 I | h -1 Fin | k f d
525 17 mptexd φ y I if y = X 1 0 V
526 elsng y I if y = X 1 0 V y I if y = X 1 0 y I if y = X 1 0 y I if y = X 1 0 = y I if y = X 1 0
527 525 526 syl φ y I if y = X 1 0 y I if y = X 1 0 y I if y = X 1 0 = y I if y = X 1 0
528 70 527 mpbiri φ y I if y = X 1 0 y I if y = X 1 0
529 528 ad2antrr φ d h 0 I | h -1 Fin v k h 0 I | h -1 Fin | k f d y I if y = X 1 0 y I if y = X 1 0
530 449 mpofun Fun f +
531 530 a1i φ d h 0 I | h -1 Fin v k h 0 I | h -1 Fin | k f d Fun f +
532 xpss k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 V × V
533 472 inex1 dom m dom n V
534 533 mptex o dom m dom n m o + n o V
535 534 rgen2w m V n V o dom m dom n m o + n o V
536 449 dmmpoga m V n V o dom m dom n m o + n o V dom f + = V × V
537 535 536 mp1i φ d h 0 I | h -1 Fin v k h 0 I | h -1 Fin | k f d dom f + = V × V
538 532 537 sseqtrrid φ d h 0 I | h -1 Fin v k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 dom f +
539 524 529 531 538 elovimad φ d h 0 I | h -1 Fin v k h 0 I | h -1 Fin | k f d v + f y I if y = X 1 0 f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0
540 17 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d I V
541 elrabi v k h 0 I | h -1 Fin | k f d v h 0 I | h -1 Fin
542 18 psrbagf v h 0 I | h -1 Fin v : I 0
543 541 542 syl v k h 0 I | h -1 Fin | k f d v : I 0
544 543 ad2antll φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d v : I 0
545 133 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d y I if y = X 1 0 : I 0
546 494 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d q 0 r 0 s 0 q + r - s = q + r - s
547 540 544 545 545 546 caofass φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d v + f y I if y = X 1 0 f y I if y = X 1 0 = v + f y I if y = X 1 0 f y I if y = X 1 0
548 135 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d y I if y = X 1 0 Fn I
549 80 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I y I if y = X 1 0 i = if i = X 1 0
550 548 548 540 540 74 549 549 offval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d y I if y = X 1 0 f y I if y = X 1 0 = i I if i = X 1 0 if i = X 1 0
551 550 oveq2d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d v + f y I if y = X 1 0 f y I if y = X 1 0 = v + f i I if i = X 1 0 if i = X 1 0
552 506 oveq2i v + f i I if i = X 1 0 if i = X 1 0 = v + f I × 0
553 0zd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d 0
554 nn0cn p 0 p
555 554 addridd p 0 p + 0 = p
556 555 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d p 0 p + 0 = p
557 540 544 553 556 caofid0r φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d v + f I × 0 = v
558 552 557 eqtrid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d v + f i I if i = X 1 0 if i = X 1 0 = v
559 547 551 558 3eqtrrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d v = v + f y I if y = X 1 0 f y I if y = X 1 0
560 oveq1 u = v + f y I if y = X 1 0 u f y I if y = X 1 0 = v + f y I if y = X 1 0 f y I if y = X 1 0
561 560 eqeq2d u = v + f y I if y = X 1 0 v = u f y I if y = X 1 0 v = v + f y I if y = X 1 0 f y I if y = X 1 0
562 559 561 syl5ibrcom φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u = v + f y I if y = X 1 0 v = u f y I if y = X 1 0
563 20 ad3antrrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d y I if y = X 1 0 h 0 I | h -1 Fin
564 18 psrbagaddcl m h 0 I | h -1 Fin y I if y = X 1 0 h 0 I | h -1 Fin m + f y I if y = X 1 0 h 0 I | h -1 Fin
565 458 563 564 syl2an2 φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 h 0 I | h -1 Fin
566 18 psrbagf m + f y I if y = X 1 0 h 0 I | h -1 Fin m + f y I if y = X 1 0 : I 0
567 565 566 syl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 : I 0
568 567 adantrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 m + f y I if y = X 1 0 : I 0
569 feq1 u = m + f y I if y = X 1 0 u : I 0 m + f y I if y = X 1 0 : I 0
570 568 569 syl5ibrcom φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f y I if y = X 1 0 u : I 0
571 485 570 sylbid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u : I 0
572 481 571 sylbird φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u : I 0
573 572 rexlimdvva φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u : I 0
574 457 573 mpd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u : I 0
575 574 adantrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u : I 0
576 575 ffvelcdmda φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I u i 0
577 576 nn0cnd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I u i
578 239 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I if i = X 1 0
579 577 578 npcand φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I u i - if i = X 1 0 + if i = X 1 0 = u i
580 579 mpteq2dva φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I u i - if i = X 1 0 + if i = X 1 0 = i I u i
581 575 ffnd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u Fn I
582 581 548 540 540 74 offn φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u f y I if y = X 1 0 Fn I
583 eqidd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I u i = u i
584 581 548 540 540 74 583 549 ofval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d i I u f y I if y = X 1 0 i = u i if i = X 1 0
585 582 548 540 540 74 584 549 offval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u f y I if y = X 1 0 + f y I if y = X 1 0 = i I u i - if i = X 1 0 + if i = X 1 0
586 575 feqmptd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u = i I u i
587 580 585 586 3eqtr4rd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u = u f y I if y = X 1 0 + f y I if y = X 1 0
588 oveq1 v = u f y I if y = X 1 0 v + f y I if y = X 1 0 = u f y I if y = X 1 0 + f y I if y = X 1 0
589 588 eqeq2d v = u f y I if y = X 1 0 u = v + f y I if y = X 1 0 u = u f y I if y = X 1 0 + f y I if y = X 1 0
590 587 589 syl5ibrcom φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d v = u f y I if y = X 1 0 u = v + f y I if y = X 1 0
591 562 590 impbid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 v k h 0 I | h -1 Fin | k f d u = v + f y I if y = X 1 0 v = u f y I if y = X 1 0
592 448 523 539 591 f1o2d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 : f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 1-1 onto k h 0 I | h -1 Fin | k f d
593 9 106 13 428 442 447 592 gsumf1o φ d h 0 I | h -1 Fin R b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b = R b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0
594 555 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d p 0 p + 0 = p
595 486 488 508 594 caofid0r φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f I × 0 = m
596 507 595 eqtrid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f i I if i = X 1 0 if i = X 1 0 = m
597 496 502 596 3eqtrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f y I if y = X 1 0 = m
598 597 514 eqeltrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
599 598 517 syl5ibrcom φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d u = m + f y I if y = X 1 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
600 599 adantrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f y I if y = X 1 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
601 485 600 sylbid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
602 481 601 sylbird φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
603 602 rexlimdvva φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
604 457 603 mpd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
605 eqidd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 = u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0
606 eqidd φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b = b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b
607 fveq2 b = u f y I if y = X 1 0 I mPSDer R X F b = I mPSDer R X F u f y I if y = X 1 0
608 oveq2 b = u f y I if y = X 1 0 d f b = d f u f y I if y = X 1 0
609 608 fveq2d b = u f y I if y = X 1 0 G d f b = G d f u f y I if y = X 1 0
610 607 609 oveq12d b = u f y I if y = X 1 0 I mPSDer R X F b R G d f b = I mPSDer R X F u f y I if y = X 1 0 R G d f u f y I if y = X 1 0
611 604 605 606 610 fmptco φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 = u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 I mPSDer R X F u f y I if y = X 1 0 R G d f u f y I if y = X 1 0
612 6 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 X I
613 7 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 F B
614 elrabi u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u f y I if y = X 1 0 h 0 I | h -1 Fin
615 604 614 syl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 h 0 I | h -1 Fin
616 1 2 18 612 613 615 psdcoef φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 I mPSDer R X F u f y I if y = X 1 0 = u f y I if y = X 1 0 X + 1 R F u f y I if y = X 1 0 + f y I if y = X 1 0
617 574 ffnd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u Fn I
618 133 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 y I if y = X 1 0 : I 0
619 618 ffnd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 y I if y = X 1 0 Fn I
620 17 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 I V
621 eqidd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 X I u X = u X
622 iftrue y = X if y = X 1 0 = 1
623 1ex 1 V
624 622 70 623 fvmpt X I y I if y = X 1 0 X = 1
625 624 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 X I y I if y = X 1 0 X = 1
626 617 619 620 620 74 621 625 ofval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 X I u f y I if y = X 1 0 X = u X 1
627 612 626 mpdan φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 X = u X 1
628 627 oveq1d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 X + 1 = u X - 1 + 1
629 nn0sscn 0
630 629 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 0
631 574 630 fssd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u : I
632 631 612 ffvelcdmd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X
633 1cnd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 1
634 632 633 npcand φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X - 1 + 1 = u X
635 628 634 eqtrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 X + 1 = u X
636 617 619 620 620 74 offn φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 Fn I
637 eqidd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I u i = u i
638 80 adantl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I y I if y = X 1 0 i = if i = X 1 0
639 617 619 620 620 74 637 638 ofval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I u f y I if y = X 1 0 i = u i if i = X 1 0
640 574 ffvelcdmda φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I u i 0
641 640 nn0cnd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I u i
642 239 a1i φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I if i = X 1 0
643 641 642 npcand φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I u i - if i = X 1 0 + if i = X 1 0 = u i
644 620 636 619 617 639 638 643 offveq φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 + f y I if y = X 1 0 = u
645 644 fveq2d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 F u f y I if y = X 1 0 + f y I if y = X 1 0 = F u
646 635 645 oveq12d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 X + 1 R F u f y I if y = X 1 0 + f y I if y = X 1 0 = u X R F u
647 616 646 eqtrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 I mPSDer R X F u f y I if y = X 1 0 = u X R F u
648 30 ad2antlr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d : I 0
649 648 ffvelcdmda φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I d i 0
650 649 nn0cnd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I d i
651 650 641 642 subsub3d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I d i u i if i = X 1 0 = d i + if i = X 1 0 - u i
652 651 mpteq2dva φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I d i u i if i = X 1 0 = i I d i + if i = X 1 0 - u i
653 67 adantr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d Fn I
654 eqidd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I d i = d i
655 653 636 620 620 74 654 639 offval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d f u f y I if y = X 1 0 = i I d i u i if i = X 1 0
656 653 619 620 620 74 offn φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d + f y I if y = X 1 0 Fn I
657 653 619 620 620 74 654 638 ofval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 i I d + f y I if y = X 1 0 i = d i + if i = X 1 0
658 656 617 620 620 74 657 637 offval φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d + f y I if y = X 1 0 f u = i I d i + if i = X 1 0 - u i
659 652 655 658 3eqtr4d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d f u f y I if y = X 1 0 = d + f y I if y = X 1 0 f u
660 659 fveq2d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 G d f u f y I if y = X 1 0 = G d + f y I if y = X 1 0 f u
661 647 660 oveq12d φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 I mPSDer R X F u f y I if y = X 1 0 R G d f u f y I if y = X 1 0 = u X R F u R G d + f y I if y = X 1 0 f u
662 11 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 R Ring
663 574 612 ffvelcdmd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X 0
664 663 nn0zd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X
665 39 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 F : h 0 I | h -1 Fin Base R
666 simpllr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 d h 0 I | h -1 Fin
667 20 ad3antrrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 y I if y = X 1 0 h 0 I | h -1 Fin
668 simprl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d
669 eqid l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0 = l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
670 18 245 669 psrbagleadd1 d h 0 I | h -1 Fin y I if y = X 1 0 h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
671 666 667 668 670 syl3anc φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 m + f y I if y = X 1 0 l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
672 eleq1 u = m + f y I if y = X 1 0 u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0 m + f y I if y = X 1 0 l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
673 671 672 syl5ibrcom φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f y I if y = X 1 0 u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
674 485 673 sylbid φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
675 481 674 sylbird φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
676 675 rexlimdvva φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
677 457 676 mpd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
678 elrabi u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0 u h 0 I | h -1 Fin
679 677 678 syl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u h 0 I | h -1 Fin
680 665 679 ffvelcdmd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 F u Base R
681 44 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 G : h 0 I | h -1 Fin Base R
682 23 adantr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d + f y I if y = X 1 0 h 0 I | h -1 Fin
683 18 669 psrbagconcl d + f y I if y = X 1 0 h 0 I | h -1 Fin u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0 d + f y I if y = X 1 0 f u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
684 682 677 683 syl2anc φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d + f y I if y = X 1 0 f u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0
685 elrabi d + f y I if y = X 1 0 f u l h 0 I | h -1 Fin | l f d + f y I if y = X 1 0 d + f y I if y = X 1 0 f u h 0 I | h -1 Fin
686 684 685 syl φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 d + f y I if y = X 1 0 f u h 0 I | h -1 Fin
687 681 686 ffvelcdmd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 G d + f y I if y = X 1 0 f u Base R
688 9 26 37 mulgass2 R Ring u X F u Base R G d + f y I if y = X 1 0 f u Base R u X R F u R G d + f y I if y = X 1 0 f u = u X R F u R G d + f y I if y = X 1 0 f u
689 662 664 680 687 688 syl13anc φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u = u X R F u R G d + f y I if y = X 1 0 f u
690 661 689 eqtrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 I mPSDer R X F u f y I if y = X 1 0 R G d f u f y I if y = X 1 0 = u X R F u R G d + f y I if y = X 1 0 f u
691 690 mpteq2dva φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 I mPSDer R X F u f y I if y = X 1 0 R G d f u f y I if y = X 1 0 = u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u
692 611 691 eqtrd φ d h 0 I | h -1 Fin b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 = u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u
693 692 oveq2d φ d h 0 I | h -1 Fin R b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 = R u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u
694 snex y I if y = X 1 0 V
695 357 694 xpex k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 V
696 695 funimaex Fun f + f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 V
697 530 696 mp1i φ d h 0 I | h -1 Fin f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 V
698 28 ad2antrr φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 R Mnd
699 9 37 662 680 687 ringcld φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 F u R G d + f y I if y = X 1 0 f u Base R
700 9 26 698 663 699 mulgnn0cld φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u Base R
701 eqid u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u = u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u
702 361 701 fnmpti u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
703 702 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u Fn k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
704 703 25 115 fndmfifsupp φ d h 0 I | h -1 Fin finSupp 0 R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u
705 462 ad2antlr φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 m Fn dom m
706 469 adantl φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 n Fn dom n
707 472 a1i φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 dom m V
708 475 a1i φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 dom n V
709 eqidd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 o dom m m o = m o
710 eqidd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 o dom n n o = n o
711 705 706 707 708 477 709 710 offval φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 m + f n = o dom m dom n m o + n o
712 711 eqeq2d φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u = o dom m dom n m o + n o
713 712 rexbidva φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n n y I if y = X 1 0 u = o dom m dom n m o + n o
714 20 ad2antrr φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d y I if y = X 1 0 h 0 I | h -1 Fin
715 oveq2 n = y I if y = X 1 0 m + f n = m + f y I if y = X 1 0
716 715 eqeq2d n = y I if y = X 1 0 u = m + f n u = m + f y I if y = X 1 0
717 716 rexsng y I if y = X 1 0 h 0 I | h -1 Fin n y I if y = X 1 0 u = m + f n u = m + f y I if y = X 1 0
718 714 717 syl φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = m + f n u = m + f y I if y = X 1 0
719 713 718 bitr3d φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o u = m + f y I if y = X 1 0
720 719 rexbidva φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d n y I if y = X 1 0 u = o dom m dom n m o + n o m k h 0 I | h -1 Fin | k f d u = m + f y I if y = X 1 0
721 breq1 k = m + f y I if y = X 1 0 k f d + f y I if y = X 1 0 m + f y I if y = X 1 0 f d + f y I if y = X 1 0
722 breq1 k = m + f y I if y = X 1 0 k f d m + f y I if y = X 1 0 f d
723 fveq1 k = m + f y I if y = X 1 0 k X = m + f y I if y = X 1 0 X
724 723 eqeq1d k = m + f y I if y = X 1 0 k X = 0 m + f y I if y = X 1 0 X = 0
725 722 724 anbi12d k = m + f y I if y = X 1 0 k f d k X = 0 m + f y I if y = X 1 0 f d m + f y I if y = X 1 0 X = 0
726 725 notbid k = m + f y I if y = X 1 0 ¬ k f d k X = 0 ¬ m + f y I if y = X 1 0 f d m + f y I if y = X 1 0 X = 0
727 721 726 anbi12d k = m + f y I if y = X 1 0 k f d + f y I if y = X 1 0 ¬ k f d k X = 0 m + f y I if y = X 1 0 f d + f y I if y = X 1 0 ¬ m + f y I if y = X 1 0 f d m + f y I if y = X 1 0 X = 0
728 458 714 564 syl2an2 φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 h 0 I | h -1 Fin
729 simplr φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d d h 0 I | h -1 Fin
730 simpr φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m k h 0 I | h -1 Fin | k f d
731 18 245 46 psrbagleadd1 d h 0 I | h -1 Fin y I if y = X 1 0 h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
732 729 714 730 731 syl3anc φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
733 721 elrab m + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 m + f y I if y = X 1 0 h 0 I | h -1 Fin m + f y I if y = X 1 0 f d + f y I if y = X 1 0
734 733 simprbi m + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 m + f y I if y = X 1 0 f d + f y I if y = X 1 0
735 732 734 syl φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f d + f y I if y = X 1 0
736 6 ad2antrr φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d X I
737 487 adantl φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m : I 0
738 737 ffnd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m Fn I
739 135 ad2antrr φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d y I if y = X 1 0 Fn I
740 17 ad2antrr φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d I V
741 eqidd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d X I m X = m X
742 624 adantl φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d X I y I if y = X 1 0 X = 1
743 738 739 740 740 74 741 742 ofval φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d X I m + f y I if y = X 1 0 X = m X + 1
744 736 743 mpdan φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 X = m X + 1
745 737 736 ffvelcdmd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m X 0
746 nn0p1nn m X 0 m X + 1
747 745 746 syl φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m X + 1
748 744 747 eqeltrd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 X
749 748 nnne0d φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 X 0
750 749 neneqd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d ¬ m + f y I if y = X 1 0 X = 0
751 750 intnand φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d ¬ m + f y I if y = X 1 0 f d m + f y I if y = X 1 0 X = 0
752 735 751 jca φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 f d + f y I if y = X 1 0 ¬ m + f y I if y = X 1 0 f d m + f y I if y = X 1 0 X = 0
753 727 728 752 elrabd φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d m + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0
754 eleq1 u = m + f y I if y = X 1 0 u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 m + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0
755 753 754 syl5ibrcom φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d u = m + f y I if y = X 1 0 u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0
756 breq1 k = u f y I if y = X 1 0 k f d u f y I if y = X 1 0 f d
757 elrabi u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u h 0 I | h -1 Fin
758 757 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u h 0 I | h -1 Fin
759 133 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 y I if y = X 1 0 : I 0
760 757 125 syl u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u : I 0
761 760 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u : I 0
762 6 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 X I
763 761 762 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X 0
764 341 notbid k = u ¬ k f d k X = 0 ¬ u f d u X = 0
765 120 764 anbi12d k = u k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f d + f y I if y = X 1 0 ¬ u f d u X = 0
766 765 elrab u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u h 0 I | h -1 Fin u f d + f y I if y = X 1 0 ¬ u f d u X = 0
767 766 simprbi u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f d + f y I if y = X 1 0 ¬ u f d u X = 0
768 767 simpld u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f d + f y I if y = X 1 0
769 768 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f d + f y I if y = X 1 0
770 769 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u f d + f y I if y = X 1 0
771 757 126 syl u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u Fn I
772 771 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u Fn I
773 772 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u Fn I
774 23 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 d + f y I if y = X 1 0 h 0 I | h -1 Fin
775 90 ffnd d + f y I if y = X 1 0 h 0 I | h -1 Fin d + f y I if y = X 1 0 Fn I
776 774 775 syl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 d + f y I if y = X 1 0 Fn I
777 776 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 d + f y I if y = X 1 0 Fn I
778 17 ad3antrrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 I V
779 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I u i = u i
780 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I d + f y I if y = X 1 0 i = d + f y I if y = X 1 0 i
781 773 777 778 778 74 779 780 ofrfval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u f d + f y I if y = X 1 0 i I u i d + f y I if y = X 1 0 i
782 770 781 mpbid φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I u i d + f y I if y = X 1 0 i
783 782 r19.21bi φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I u i d + f y I if y = X 1 0 i
784 783 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X u i d + f y I if y = X 1 0 i
785 67 ad3antrrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i X d Fn I
786 71 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i X y I if y = X 1 0 Fn I
787 17 ad4antr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i X I V
788 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i X i I d i = d i
789 80 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i X i I y I if y = X 1 0 i = if i = X 1 0
790 785 786 787 787 74 788 789 ofval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i X i I d + f y I if y = X 1 0 i = d i + if i = X 1 0
791 790 an32s φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X d + f y I if y = X 1 0 i = d i + if i = X 1 0
792 160 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X if i = X 1 0 = 0
793 792 oveq2d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X d i + if i = X 1 0 = d i + 0
794 31 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 d : I 0
795 794 ffvelcdmda φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I d i 0
796 795 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X d i 0
797 796 nn0cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X d i
798 797 addridd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X d i + 0 = d i
799 791 793 798 3eqtrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X d + f y I if y = X 1 0 i = d i
800 784 799 breqtrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I i X u i d i
801 simpr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u X = 0
802 31 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 d : I 0
803 802 762 ffvelcdmd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 d X 0
804 803 nn0ge0d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 0 d X
805 804 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 0 d X
806 801 805 eqbrtrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u X d X
807 806 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I u X d X
808 177 800 807 pm2.61ne φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I u i d i
809 808 ralrimiva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I u i d i
810 67 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 d Fn I
811 810 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 d Fn I
812 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 i I d i = d i
813 773 811 778 778 74 779 812 ofrfval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u f d i I u i d i
814 809 813 mpbird φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u f d
815 814 ex φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 u f d
816 767 simprd u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 ¬ u f d u X = 0
817 816 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 ¬ u f d u X = 0
818 imnan u f d ¬ u X = 0 ¬ u f d u X = 0
819 817 818 sylibr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f d ¬ u X = 0
820 819 con2d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X = 0 ¬ u f d
821 815 820 pm2.65d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 ¬ u X = 0
822 821 neqned φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X 0
823 763 822 193 sylanbrc φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u X
824 823 nnge1d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 1 u X
825 824 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I 1 u X
826 175 breq2d i = X 1 u i 1 u X
827 825 826 syl5ibrcom φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I i = X 1 u i
828 827 imp φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I i = X 1 u i
829 761 ffvelcdmda φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i 0
830 829 nn0ge0d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I 0 u i
831 830 adantr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I ¬ i = X 0 u i
832 828 831 ifpimpda φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I if- i = X 1 u i 0 u i
833 brif1 if i = X 1 0 u i if- i = X 1 u i 0 u i
834 832 833 sylibr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I if i = X 1 0 u i
835 834 ralrimiva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I if i = X 1 0 u i
836 71 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 y I if y = X 1 0 Fn I
837 17 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 I V
838 80 adantl φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I y I if y = X 1 0 i = if i = X 1 0
839 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i = u i
840 836 772 837 837 74 838 839 ofrfval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 y I if y = X 1 0 f u i I if i = X 1 0 u i
841 835 840 mpbird φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 y I if y = X 1 0 f u
842 18 psrbagcon u h 0 I | h -1 Fin y I if y = X 1 0 : I 0 y I if y = X 1 0 f u u f y I if y = X 1 0 h 0 I | h -1 Fin u f y I if y = X 1 0 f u
843 758 759 841 842 syl3anc φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f y I if y = X 1 0 h 0 I | h -1 Fin u f y I if y = X 1 0 f u
844 843 simpld φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f y I if y = X 1 0 h 0 I | h -1 Fin
845 eqidd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I d i = d i
846 810 836 837 837 74 845 838 ofval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I d + f y I if y = X 1 0 i = d i + if i = X 1 0
847 772 776 837 837 74 839 846 ofrfval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f d + f y I if y = X 1 0 i I u i d i + if i = X 1 0
848 769 847 mpbid φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i d i + if i = X 1 0
849 848 r19.21bi φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i d i + if i = X 1 0
850 829 nn0red φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i
851 62 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I if i = X 1 0
852 802 ffvelcdmda φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I d i 0
853 852 nn0red φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I d i
854 850 851 853 lesubaddd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i if i = X 1 0 d i u i d i + if i = X 1 0
855 849 854 mpbird φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i if i = X 1 0 d i
856 855 ralrimiva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i if i = X 1 0 d i
857 772 836 837 837 74 offn φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f y I if y = X 1 0 Fn I
858 772 836 837 837 74 839 838 ofval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u f y I if y = X 1 0 i = u i if i = X 1 0
859 857 810 837 837 74 858 845 ofrfval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f y I if y = X 1 0 f d i I u i if i = X 1 0 d i
860 856 859 mpbird φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f y I if y = X 1 0 f d
861 756 844 860 elrabd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d
862 829 nn0cnd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i
863 239 a1i φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I if i = X 1 0
864 862 863 npcand φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i - if i = X 1 0 + if i = X 1 0 = u i
865 864 mpteq2dva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 i I u i - if i = X 1 0 + if i = X 1 0 = i I u i
866 857 836 837 837 74 858 838 offval φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u f y I if y = X 1 0 + f y I if y = X 1 0 = i I u i - if i = X 1 0 + if i = X 1 0
867 761 feqmptd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u = i I u i
868 865 866 867 3eqtr4rd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0 u = u f y I if y = X 1 0 + f y I if y = X 1 0
869 oveq1 m = u f y I if y = X 1 0 m + f y I if y = X 1 0 = u f y I if y = X 1 0 + f y I if y = X 1 0
870 869 eqeq2d m = u f y I if y = X 1 0 u = m + f y I if y = X 1 0 u = u f y I if y = X 1 0 + f y I if y = X 1 0
871 755 861 868 870 rspceb2dv φ d h 0 I | h -1 Fin m k h 0 I | h -1 Fin | k f d u = m + f y I if y = X 1 0 u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0
872 456 720 871 3bitrd φ d h 0 I | h -1 Fin u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0
873 872 eqrdv φ d h 0 I | h -1 Fin f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0
874 difrab k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k X = 0 = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 ¬ k f d k X = 0
875 873 874 eqtr4di φ d h 0 I | h -1 Fin f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k X = 0
876 difssd φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
877 875 876 eqsstrd φ d h 0 I | h -1 Fin f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0
878 704 877 115 fmptssfisupp φ d h 0 I | h -1 Fin finSupp 0 R u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u
879 difss k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d
880 disjdif k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d =
881 ssdisj k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d = k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d =
882 879 880 881 mp2an k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d =
883 882 ineqcomi k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 =
884 883 a1i φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 =
885 281 101 psdmullem φ d h 0 I | h -1 Fin k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k X = 0
886 875 885 eqtr4d φ d h 0 I | h -1 Fin f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 = k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0
887 9 106 10 13 697 700 878 884 886 gsumsplit2 φ d h 0 I | h -1 Fin R u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u X R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u
888 693 887 eqtrd φ d h 0 I | h -1 Fin R b k h 0 I | h -1 Fin | k f d I mPSDer R X F b R G d f b u f + k h 0 I | h -1 Fin | k f d × y I if y = X 1 0 u f y I if y = X 1 0 = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u
889 427 593 888 3eqtrd φ d h 0 I | h -1 Fin I mPSDer R X F · ˙ G d = R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u
890 417 adantr φ d h 0 I | h -1 Fin I mPSDer R X G B
891 1 2 37 4 18 387 890 14 psrmulval φ d h 0 I | h -1 Fin F · ˙ I mPSDer R X G d = R u k h 0 I | h -1 Fin | k f d F u R I mPSDer R X G d f u
892 8 ad2antrr φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d G B
893 1 2 18 287 892 249 psdcoef φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d I mPSDer R X G d f u = d f u X + 1 R G d f u + f y I if y = X 1 0
894 269 fveq2d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d G d f u + f y I if y = X 1 0 = G d + f y I if y = X 1 0 f u
895 894 oveq2d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u X + 1 R G d f u + f y I if y = X 1 0 = d f u X + 1 R G d + f y I if y = X 1 0 f u
896 893 895 eqtrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d I mPSDer R X G d f u = d f u X + 1 R G d + f y I if y = X 1 0 f u
897 896 oveq2d φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d F u R I mPSDer R X G d f u = F u R d f u X + 1 R G d + f y I if y = X 1 0 f u
898 311 nn0zd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d d f u X + 1
899 9 26 37 mulgass3 R Ring d f u X + 1 F u Base R G d + f y I if y = X 1 0 f u Base R F u R d f u X + 1 R G d + f y I if y = X 1 0 f u = d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
900 226 898 230 273 899 syl13anc φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d F u R d f u X + 1 R G d + f y I if y = X 1 0 f u = d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
901 897 900 eqtrd φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d F u R I mPSDer R X G d f u = d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
902 901 mpteq2dva φ d h 0 I | h -1 Fin u k h 0 I | h -1 Fin | k f d F u R I mPSDer R X G d f u = u k h 0 I | h -1 Fin | k f d d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
903 902 oveq2d φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d F u R I mPSDer R X G d f u = R u k h 0 I | h -1 Fin | k f d d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
904 9 10 13 223 323 277 284 gsummptfidmsplit φ d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d d f u X + 1 R F u R G d + f y I if y = X 1 0 f u = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
905 891 903 904 3eqtrd φ d h 0 I | h -1 Fin F · ˙ I mPSDer R X G d = R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
906 421 423 424 424 425 889 905 offval φ I mPSDer R X F · ˙ G + R f F · ˙ I mPSDer R X G = d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
907 419 906 eqtrd φ I mPSDer R X F · ˙ G + ˙ F · ˙ I mPSDer R X G = d h 0 I | h -1 Fin R u k h 0 I | h -1 Fin | k f d + f y I if y = X 1 0 k h 0 I | h -1 Fin | k f d u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 u X R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u + R R u k h 0 I | h -1 Fin | k f d k X = 0 d f u X + 1 R F u R G d + f y I if y = X 1 0 f u
908 411 413 907 3eqtr4d φ I mPSDer R X F · ˙ G = I mPSDer R X F · ˙ G + ˙ F · ˙ I mPSDer R X G