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