Metamath Proof Explorer


Theorem sdclem1

Description: Lemma for sdc . (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses sdc.1 Z = M
sdc.2 g = f M n ψ χ
sdc.3 n = M ψ τ
sdc.4 n = k ψ θ
sdc.5 g = h n = k + 1 ψ σ
sdc.6 φ A V
sdc.7 φ M
sdc.8 φ g g : M A τ
sdc.9 φ k Z g : M k A θ h h : M k + 1 A g = h M k σ
sdc.10 J = g | n Z g : M n A ψ
sdc.11 F = w Z , x J h | k Z h : M k + 1 A x = h M k σ
Assertion sdclem1 φ f f : Z A n Z χ

Proof

Step Hyp Ref Expression
1 sdc.1 Z = M
2 sdc.2 g = f M n ψ χ
3 sdc.3 n = M ψ τ
4 sdc.4 n = k ψ θ
5 sdc.5 g = h n = k + 1 ψ σ
6 sdc.6 φ A V
7 sdc.7 φ M
8 sdc.8 φ g g : M A τ
9 sdc.9 φ k Z g : M k A θ h h : M k + 1 A g = h M k σ
10 sdc.10 J = g | n Z g : M n A ψ
11 sdc.11 F = w Z , x J h | k Z h : M k + 1 A x = h M k σ
12 1 fvexi Z V
13 simpl g : M n A ψ g : M n A
14 ovex M n V
15 elmapg A V M n V g A M n g : M n A
16 6 14 15 sylancl φ g A M n g : M n A
17 13 16 syl5ibr φ g : M n A ψ g A M n
18 17 abssdv φ g | g : M n A ψ A M n
19 ovex A M n V
20 ssexg g | g : M n A ψ A M n A M n V g | g : M n A ψ V
21 18 19 20 sylancl φ g | g : M n A ψ V
22 21 ralrimivw φ n Z g | g : M n A ψ V
23 abrexex2g Z V n Z g | g : M n A ψ V g | n Z g : M n A ψ V
24 12 22 23 sylancr φ g | n Z g : M n A ψ V
25 10 24 eqeltrid φ J V
26 25 adantr φ g : M A τ J V
27 7 adantr φ g : M A τ M
28 uzid M M M
29 27 28 syl φ g : M A τ M M
30 29 1 eleqtrrdi φ g : M A τ M Z
31 simprl φ g : M A τ g : M A
32 fzsn M M M = M
33 27 32 syl φ g : M A τ M M = M
34 33 feq2d φ g : M A τ g : M M A g : M A
35 31 34 mpbird φ g : M A τ g : M M A
36 simprr φ g : M A τ τ
37 oveq2 n = M M n = M M
38 37 feq2d n = M g : M n A g : M M A
39 38 3 anbi12d n = M g : M n A ψ g : M M A τ
40 39 rspcev M Z g : M M A τ n Z g : M n A ψ
41 30 35 36 40 syl12anc φ g : M A τ n Z g : M n A ψ
42 10 abeq2i g J n Z g : M n A ψ
43 41 42 sylibr φ g : M A τ g J
44 1 peano2uzs k Z k + 1 Z
45 44 ad2antlr φ k Z h : M k + 1 A x = h M k σ k + 1 Z
46 simpr1 φ k Z h : M k + 1 A x = h M k σ h : M k + 1 A
47 simpr3 φ k Z h : M k + 1 A x = h M k σ σ
48 vex h V
49 ovex k + 1 V
50 5 a1i φ g = h n = k + 1 ψ σ
51 48 49 50 sbc2iedv φ [˙h / g]˙ [˙k + 1 / n]˙ ψ σ
52 51 ad2antrr φ k Z h : M k + 1 A x = h M k σ [˙h / g]˙ [˙k + 1 / n]˙ ψ σ
53 47 52 mpbird φ k Z h : M k + 1 A x = h M k σ [˙h / g]˙ [˙k + 1 / n]˙ ψ
54 nfv n h : M k + 1 A
55 nfcv _ n h
56 nfsbc1v n [˙k + 1 / n]˙ ψ
57 55 56 nfsbcw n [˙h / g]˙ [˙k + 1 / n]˙ ψ
58 54 57 nfan n h : M k + 1 A [˙h / g]˙ [˙k + 1 / n]˙ ψ
59 oveq2 n = k + 1 M n = M k + 1
60 59 feq2d n = k + 1 h : M n A h : M k + 1 A
61 sbceq1a n = k + 1 ψ [˙k + 1 / n]˙ ψ
62 61 sbcbidv n = k + 1 [˙h / g]˙ ψ [˙h / g]˙ [˙k + 1 / n]˙ ψ
63 60 62 anbi12d n = k + 1 h : M n A [˙h / g]˙ ψ h : M k + 1 A [˙h / g]˙ [˙k + 1 / n]˙ ψ
64 58 63 rspce k + 1 Z h : M k + 1 A [˙h / g]˙ [˙k + 1 / n]˙ ψ n Z h : M n A [˙h / g]˙ ψ
65 45 46 53 64 syl12anc φ k Z h : M k + 1 A x = h M k σ n Z h : M n A [˙h / g]˙ ψ
66 10 eleq2i h J h g | n Z g : M n A ψ
67 nfcv _ g Z
68 nfv g h : M n A
69 nfsbc1v g [˙h / g]˙ ψ
70 68 69 nfan g h : M n A [˙h / g]˙ ψ
71 67 70 nfrex g n Z h : M n A [˙h / g]˙ ψ
72 feq1 g = h g : M n A h : M n A
73 sbceq1a g = h ψ [˙h / g]˙ ψ
74 72 73 anbi12d g = h g : M n A ψ h : M n A [˙h / g]˙ ψ
75 74 rexbidv g = h n Z g : M n A ψ n Z h : M n A [˙h / g]˙ ψ
76 71 48 75 elabf h g | n Z g : M n A ψ n Z h : M n A [˙h / g]˙ ψ
77 66 76 bitri h J n Z h : M n A [˙h / g]˙ ψ
78 65 77 sylibr φ k Z h : M k + 1 A x = h M k σ h J
79 78 rexlimdva2 φ k Z h : M k + 1 A x = h M k σ h J
80 79 abssdv φ h | k Z h : M k + 1 A x = h M k σ J
81 80 ad2antrr φ g : M A τ x J h | k Z h : M k + 1 A x = h M k σ J
82 25 ad2antrr φ g : M A τ x J J V
83 elpw2g J V h | k Z h : M k + 1 A x = h M k σ 𝒫 J h | k Z h : M k + 1 A x = h M k σ J
84 82 83 syl φ g : M A τ x J h | k Z h : M k + 1 A x = h M k σ 𝒫 J h | k Z h : M k + 1 A x = h M k σ J
85 81 84 mpbird φ g : M A τ x J h | k Z h : M k + 1 A x = h M k σ 𝒫 J
86 oveq2 n = k M n = M k
87 86 feq2d n = k g : M n A g : M k A
88 87 4 anbi12d n = k g : M n A ψ g : M k A θ
89 88 cbvrexvw n Z g : M n A ψ k Z g : M k A θ
90 9 reximdva φ k Z g : M k A θ k Z h h : M k + 1 A g = h M k σ
91 rexcom4 k Z h h : M k + 1 A g = h M k σ h k Z h : M k + 1 A g = h M k σ
92 90 91 syl6ib φ k Z g : M k A θ h k Z h : M k + 1 A g = h M k σ
93 89 92 syl5bi φ n Z g : M n A ψ h k Z h : M k + 1 A g = h M k σ
94 93 ss2abdv φ g | n Z g : M n A ψ g | h k Z h : M k + 1 A g = h M k σ
95 10 94 eqsstrid φ J g | h k Z h : M k + 1 A g = h M k σ
96 95 sselda φ x J x g | h k Z h : M k + 1 A g = h M k σ
97 vex x V
98 eqeq1 g = x g = h M k x = h M k
99 98 3anbi2d g = x h : M k + 1 A g = h M k σ h : M k + 1 A x = h M k σ
100 99 rexbidv g = x k Z h : M k + 1 A g = h M k σ k Z h : M k + 1 A x = h M k σ
101 100 exbidv g = x h k Z h : M k + 1 A g = h M k σ h k Z h : M k + 1 A x = h M k σ
102 97 101 elab x g | h k Z h : M k + 1 A g = h M k σ h k Z h : M k + 1 A x = h M k σ
103 96 102 sylib φ x J h k Z h : M k + 1 A x = h M k σ
104 abn0 h | k Z h : M k + 1 A x = h M k σ h k Z h : M k + 1 A x = h M k σ
105 103 104 sylibr φ x J h | k Z h : M k + 1 A x = h M k σ
106 105 adantlr φ g : M A τ x J h | k Z h : M k + 1 A x = h M k σ
107 eldifsn h | k Z h : M k + 1 A x = h M k σ 𝒫 J h | k Z h : M k + 1 A x = h M k σ 𝒫 J h | k Z h : M k + 1 A x = h M k σ
108 85 106 107 sylanbrc φ g : M A τ x J h | k Z h : M k + 1 A x = h M k σ 𝒫 J
109 108 adantrl φ g : M A τ w Z x J h | k Z h : M k + 1 A x = h M k σ 𝒫 J
110 109 ralrimivva φ g : M A τ w Z x J h | k Z h : M k + 1 A x = h M k σ 𝒫 J
111 11 fmpo w Z x J h | k Z h : M k + 1 A x = h M k σ 𝒫 J F : Z × J 𝒫 J
112 110 111 sylib φ g : M A τ F : Z × J 𝒫 J
113 7 iftrued φ if M M 0 = M
114 113 fveq2d φ if M M 0 = M
115 114 1 eqtr4di φ if M M 0 = Z
116 115 xpeq1d φ if M M 0 × J = Z × J
117 116 feq2d φ F : if M M 0 × J 𝒫 J F : Z × J 𝒫 J
118 117 biimpar φ F : Z × J 𝒫 J F : if M M 0 × J 𝒫 J
119 112 118 syldan φ g : M A τ F : if M M 0 × J 𝒫 J
120 0z 0
121 120 elimel if M M 0
122 eqid if M M 0 = if M M 0
123 121 122 axdc4uz J V g J F : if M M 0 × J 𝒫 J j j : if M M 0 J j if M M 0 = g m if M M 0 j m + 1 m F j m
124 26 43 119 123 syl3anc φ g : M A τ j j : if M M 0 J j if M M 0 = g m if M M 0 j m + 1 m F j m
125 27 iftrued φ g : M A τ if M M 0 = M
126 125 fveq2d φ g : M A τ if M M 0 = M
127 126 1 eqtr4di φ g : M A τ if M M 0 = Z
128 127 feq2d φ g : M A τ j : if M M 0 J j : Z J
129 89 abbii g | n Z g : M n A ψ = g | k Z g : M k A θ
130 10 129 eqtri J = g | k Z g : M k A θ
131 feq3 J = g | k Z g : M k A θ j : Z J j : Z g | k Z g : M k A θ
132 130 131 ax-mp j : Z J j : Z g | k Z g : M k A θ
133 128 132 bitrdi φ g : M A τ j : if M M 0 J j : Z g | k Z g : M k A θ
134 125 fveqeq2d φ g : M A τ j if M M 0 = g j M = g
135 127 raleqdv φ g : M A τ m if M M 0 j m + 1 m F j m m Z j m + 1 m F j m
136 133 134 135 3anbi123d φ g : M A τ j : if M M 0 J j if M M 0 = g m if M M 0 j m + 1 m F j m j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m
137 6 ad2antrr φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m A V
138 7 ad2antrr φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m M
139 8 ad2antrr φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m g g : M A τ
140 simpll φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m φ
141 140 9 sylan φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m k Z g : M k A θ h h : M k + 1 A g = h M k σ
142 nfv k φ g : M A τ
143 nfcv _ k j
144 nfcv _ k Z
145 nfre1 k k Z g : M k A θ
146 145 nfab _ k g | k Z g : M k A θ
147 143 144 146 nff k j : Z g | k Z g : M k A θ
148 nfv k j M = g
149 nfcv _ k m
150 130 146 nfcxfr _ k J
151 nfre1 k k Z h : M k + 1 A x = h M k σ
152 151 nfab _ k h | k Z h : M k + 1 A x = h M k σ
153 144 150 152 nfmpo _ k w Z , x J h | k Z h : M k + 1 A x = h M k σ
154 11 153 nfcxfr _ k F
155 nfcv _ k j m
156 149 154 155 nfov _ k m F j m
157 156 nfel2 k j m + 1 m F j m
158 144 157 nfralw k m Z j m + 1 m F j m
159 147 148 158 nf3an k j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m
160 142 159 nfan k φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m
161 simpr1 φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m j : Z g | k Z g : M k A θ
162 161 132 sylibr φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m j : Z J
163 31 adantr φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m g : M A
164 simpr2 φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m j M = g
165 138 32 syl φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m M M = M
166 164 165 feq12d φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m j M : M M A g : M A
167 163 166 mpbird φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m j M : M M A
168 simpr3 φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m m Z j m + 1 m F j m
169 fvoveq1 m = w j m + 1 = j w + 1
170 id m = w m = w
171 fveq2 m = w j m = j w
172 170 171 oveq12d m = w m F j m = w F j w
173 169 172 eleq12d m = w j m + 1 m F j m j w + 1 w F j w
174 173 rspccva m Z j m + 1 m F j m w Z j w + 1 w F j w
175 168 174 sylan φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m w Z j w + 1 w F j w
176 1 2 3 4 5 137 138 139 141 10 11 160 162 167 175 sdclem2 φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m f f : Z A n Z χ
177 176 ex φ g : M A τ j : Z g | k Z g : M k A θ j M = g m Z j m + 1 m F j m f f : Z A n Z χ
178 136 177 sylbid φ g : M A τ j : if M M 0 J j if M M 0 = g m if M M 0 j m + 1 m F j m f f : Z A n Z χ
179 178 exlimdv φ g : M A τ j j : if M M 0 J j if M M 0 = g m if M M 0 j m + 1 m F j m f f : Z A n Z χ
180 124 179 mpd φ g : M A τ f f : Z A n Z χ
181 8 180 exlimddv φ f f : Z A n Z χ