Metamath Proof Explorer


Theorem pf1ind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pf1ind.cb B = Base R
pf1ind.cp + ˙ = + R
pf1ind.ct · ˙ = R
pf1ind.cq Q = ran eval 1 R
pf1ind.ad φ f Q τ g Q η ζ
pf1ind.mu φ f Q τ g Q η σ
pf1ind.wa x = B × f ψ χ
pf1ind.wb x = I B ψ θ
pf1ind.wc x = f ψ τ
pf1ind.wd x = g ψ η
pf1ind.we x = f + ˙ f g ψ ζ
pf1ind.wf x = f · ˙ f g ψ σ
pf1ind.wg x = A ψ ρ
pf1ind.co φ f B χ
pf1ind.pr φ θ
pf1ind.a φ A Q
Assertion pf1ind φ ρ

Proof

Step Hyp Ref Expression
1 pf1ind.cb B = Base R
2 pf1ind.cp + ˙ = + R
3 pf1ind.ct · ˙ = R
4 pf1ind.cq Q = ran eval 1 R
5 pf1ind.ad φ f Q τ g Q η ζ
6 pf1ind.mu φ f Q τ g Q η σ
7 pf1ind.wa x = B × f ψ χ
8 pf1ind.wb x = I B ψ θ
9 pf1ind.wc x = f ψ τ
10 pf1ind.wd x = g ψ η
11 pf1ind.we x = f + ˙ f g ψ ζ
12 pf1ind.wf x = f · ˙ f g ψ σ
13 pf1ind.wg x = A ψ ρ
14 pf1ind.co φ f B χ
15 pf1ind.pr φ θ
16 pf1ind.a φ A Q
17 coass A b B 1 𝑜 b w B 1 𝑜 × w = A b B 1 𝑜 b w B 1 𝑜 × w
18 df1o2 1 𝑜 =
19 1 fvexi B V
20 0ex V
21 eqid b B 1 𝑜 b = b B 1 𝑜 b
22 18 19 20 21 mapsncnv b B 1 𝑜 b -1 = w B 1 𝑜 × w
23 22 coeq2i b B 1 𝑜 b b B 1 𝑜 b -1 = b B 1 𝑜 b w B 1 𝑜 × w
24 18 19 20 21 mapsnf1o2 b B 1 𝑜 b : B 1 𝑜 1-1 onto B
25 f1ococnv2 b B 1 𝑜 b : B 1 𝑜 1-1 onto B b B 1 𝑜 b b B 1 𝑜 b -1 = I B
26 24 25 mp1i φ b B 1 𝑜 b b B 1 𝑜 b -1 = I B
27 23 26 eqtr3id φ b B 1 𝑜 b w B 1 𝑜 × w = I B
28 27 coeq2d φ A b B 1 𝑜 b w B 1 𝑜 × w = A I B
29 17 28 eqtrid φ A b B 1 𝑜 b w B 1 𝑜 × w = A I B
30 4 1 pf1f A Q A : B B
31 fcoi1 A : B B A I B = A
32 16 30 31 3syl φ A I B = A
33 29 32 eqtrd φ A b B 1 𝑜 b w B 1 𝑜 × w = A
34 eqid 1 𝑜 eval R = 1 𝑜 eval R
35 34 1 evlval 1 𝑜 eval R = 1 𝑜 evalSub R B
36 35 rneqi ran 1 𝑜 eval R = ran 1 𝑜 evalSub R B
37 an4 a ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b ran 1 𝑜 eval R b w B 1 𝑜 × w x | ψ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ
38 eqid ran 1 𝑜 eval R = ran 1 𝑜 eval R
39 4 1 38 mpfpf1 a ran 1 𝑜 eval R a w B 1 𝑜 × w Q
40 4 1 38 mpfpf1 b ran 1 𝑜 eval R b w B 1 𝑜 × w Q
41 vex f V
42 41 9 elab f x | ψ τ
43 eleq1 f = a w B 1 𝑜 × w f x | ψ a w B 1 𝑜 × w x | ψ
44 42 43 bitr3id f = a w B 1 𝑜 × w τ a w B 1 𝑜 × w x | ψ
45 44 anbi1d f = a w B 1 𝑜 × w τ η a w B 1 𝑜 × w x | ψ η
46 45 anbi1d f = a w B 1 𝑜 × w τ η φ a w B 1 𝑜 × w x | ψ η φ
47 ovex f + ˙ f g V
48 47 11 elab f + ˙ f g x | ψ ζ
49 oveq1 f = a w B 1 𝑜 × w f + ˙ f g = a w B 1 𝑜 × w + ˙ f g
50 49 eleq1d f = a w B 1 𝑜 × w f + ˙ f g x | ψ a w B 1 𝑜 × w + ˙ f g x | ψ
51 48 50 bitr3id f = a w B 1 𝑜 × w ζ a w B 1 𝑜 × w + ˙ f g x | ψ
52 46 51 imbi12d f = a w B 1 𝑜 × w τ η φ ζ a w B 1 𝑜 × w x | ψ η φ a w B 1 𝑜 × w + ˙ f g x | ψ
53 vex g V
54 53 10 elab g x | ψ η
55 eleq1 g = b w B 1 𝑜 × w g x | ψ b w B 1 𝑜 × w x | ψ
56 54 55 bitr3id g = b w B 1 𝑜 × w η b w B 1 𝑜 × w x | ψ
57 56 anbi2d g = b w B 1 𝑜 × w a w B 1 𝑜 × w x | ψ η a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ
58 57 anbi1d g = b w B 1 𝑜 × w a w B 1 𝑜 × w x | ψ η φ a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ φ
59 oveq2 g = b w B 1 𝑜 × w a w B 1 𝑜 × w + ˙ f g = a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w
60 59 eleq1d g = b w B 1 𝑜 × w a w B 1 𝑜 × w + ˙ f g x | ψ a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w x | ψ
61 58 60 imbi12d g = b w B 1 𝑜 × w a w B 1 𝑜 × w x | ψ η φ a w B 1 𝑜 × w + ˙ f g x | ψ a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ φ a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w x | ψ
62 5 expcom f Q τ g Q η φ ζ
63 62 an4s f Q g Q τ η φ ζ
64 63 expimpd f Q g Q τ η φ ζ
65 52 61 64 vtocl2ga a w B 1 𝑜 × w Q b w B 1 𝑜 × w Q a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ φ a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w x | ψ
66 39 40 65 syl2an a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ φ a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w x | ψ
67 66 expcomd a ran 1 𝑜 eval R b ran 1 𝑜 eval R φ a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w x | ψ
68 67 impcom φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w x | ψ
69 36 1 mpff a ran 1 𝑜 eval R a : B 1 𝑜 B
70 69 ad2antrl φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a : B 1 𝑜 B
71 70 ffnd φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a Fn B 1 𝑜
72 36 1 mpff b ran 1 𝑜 eval R b : B 1 𝑜 B
73 72 ad2antll φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R b : B 1 𝑜 B
74 73 ffnd φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R b Fn B 1 𝑜
75 eqid w B 1 𝑜 × w = w B 1 𝑜 × w
76 18 19 20 75 mapsnf1o3 w B 1 𝑜 × w : B 1-1 onto B 1 𝑜
77 f1of w B 1 𝑜 × w : B 1-1 onto B 1 𝑜 w B 1 𝑜 × w : B B 1 𝑜
78 76 77 mp1i φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R w B 1 𝑜 × w : B B 1 𝑜
79 ovexd φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R B 1 𝑜 V
80 19 a1i φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R B V
81 inidm B 1 𝑜 B 1 𝑜 = B 1 𝑜
82 71 74 78 79 79 80 81 ofco φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a + ˙ f b w B 1 𝑜 × w = a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w
83 82 eleq1d φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a + ˙ f b w B 1 𝑜 × w x | ψ a w B 1 𝑜 × w + ˙ f b w B 1 𝑜 × w x | ψ
84 68 83 sylibrd φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a + ˙ f b w B 1 𝑜 × w x | ψ
85 84 expimpd φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a + ˙ f b w B 1 𝑜 × w x | ψ
86 37 85 syl5bi φ a ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b ran 1 𝑜 eval R b w B 1 𝑜 × w x | ψ a + ˙ f b w B 1 𝑜 × w x | ψ
87 86 imp φ a ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b ran 1 𝑜 eval R b w B 1 𝑜 × w x | ψ a + ˙ f b w B 1 𝑜 × w x | ψ
88 ovex f · ˙ f g V
89 88 12 elab f · ˙ f g x | ψ σ
90 oveq1 f = a w B 1 𝑜 × w f · ˙ f g = a w B 1 𝑜 × w · ˙ f g
91 90 eleq1d f = a w B 1 𝑜 × w f · ˙ f g x | ψ a w B 1 𝑜 × w · ˙ f g x | ψ
92 89 91 bitr3id f = a w B 1 𝑜 × w σ a w B 1 𝑜 × w · ˙ f g x | ψ
93 46 92 imbi12d f = a w B 1 𝑜 × w τ η φ σ a w B 1 𝑜 × w x | ψ η φ a w B 1 𝑜 × w · ˙ f g x | ψ
94 oveq2 g = b w B 1 𝑜 × w a w B 1 𝑜 × w · ˙ f g = a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w
95 94 eleq1d g = b w B 1 𝑜 × w a w B 1 𝑜 × w · ˙ f g x | ψ a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w x | ψ
96 58 95 imbi12d g = b w B 1 𝑜 × w a w B 1 𝑜 × w x | ψ η φ a w B 1 𝑜 × w · ˙ f g x | ψ a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ φ a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w x | ψ
97 6 expcom f Q τ g Q η φ σ
98 97 an4s f Q g Q τ η φ σ
99 98 expimpd f Q g Q τ η φ σ
100 93 96 99 vtocl2ga a w B 1 𝑜 × w Q b w B 1 𝑜 × w Q a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ φ a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w x | ψ
101 39 40 100 syl2an a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ φ a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w x | ψ
102 101 expcomd a ran 1 𝑜 eval R b ran 1 𝑜 eval R φ a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w x | ψ
103 102 impcom φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w x | ψ
104 71 74 78 79 79 80 81 ofco φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a · ˙ f b w B 1 𝑜 × w = a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w
105 104 eleq1d φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a · ˙ f b w B 1 𝑜 × w x | ψ a w B 1 𝑜 × w · ˙ f b w B 1 𝑜 × w x | ψ
106 103 105 sylibrd φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a · ˙ f b w B 1 𝑜 × w x | ψ
107 106 expimpd φ a ran 1 𝑜 eval R b ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ a · ˙ f b w B 1 𝑜 × w x | ψ
108 37 107 syl5bi φ a ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b ran 1 𝑜 eval R b w B 1 𝑜 × w x | ψ a · ˙ f b w B 1 𝑜 × w x | ψ
109 108 imp φ a ran 1 𝑜 eval R a w B 1 𝑜 × w x | ψ b ran 1 𝑜 eval R b w B 1 𝑜 × w x | ψ a · ˙ f b w B 1 𝑜 × w x | ψ
110 coeq1 y = B 1 𝑜 × a y w B 1 𝑜 × w = B 1 𝑜 × a w B 1 𝑜 × w
111 110 eleq1d y = B 1 𝑜 × a y w B 1 𝑜 × w x | ψ B 1 𝑜 × a w B 1 𝑜 × w x | ψ
112 coeq1 y = b B 1 𝑜 b a y w B 1 𝑜 × w = b B 1 𝑜 b a w B 1 𝑜 × w
113 112 eleq1d y = b B 1 𝑜 b a y w B 1 𝑜 × w x | ψ b B 1 𝑜 b a w B 1 𝑜 × w x | ψ
114 coeq1 y = a y w B 1 𝑜 × w = a w B 1 𝑜 × w
115 114 eleq1d y = a y w B 1 𝑜 × w x | ψ a w B 1 𝑜 × w x | ψ
116 coeq1 y = b y w B 1 𝑜 × w = b w B 1 𝑜 × w
117 116 eleq1d y = b y w B 1 𝑜 × w x | ψ b w B 1 𝑜 × w x | ψ
118 coeq1 y = a + ˙ f b y w B 1 𝑜 × w = a + ˙ f b w B 1 𝑜 × w
119 118 eleq1d y = a + ˙ f b y w B 1 𝑜 × w x | ψ a + ˙ f b w B 1 𝑜 × w x | ψ
120 coeq1 y = a · ˙ f b y w B 1 𝑜 × w = a · ˙ f b w B 1 𝑜 × w
121 120 eleq1d y = a · ˙ f b y w B 1 𝑜 × w x | ψ a · ˙ f b w B 1 𝑜 × w x | ψ
122 coeq1 y = A b B 1 𝑜 b y w B 1 𝑜 × w = A b B 1 𝑜 b w B 1 𝑜 × w
123 122 eleq1d y = A b B 1 𝑜 b y w B 1 𝑜 × w x | ψ A b B 1 𝑜 b w B 1 𝑜 × w x | ψ
124 4 pf1rcl A Q R CRing
125 16 124 syl φ R CRing
126 125 adantr φ a B R CRing
127 1on 1 𝑜 On
128 eqid 1 𝑜 mPoly R = 1 𝑜 mPoly R
129 128 mplassa 1 𝑜 On R CRing 1 𝑜 mPoly R AssAlg
130 127 125 129 sylancr φ 1 𝑜 mPoly R AssAlg
131 eqid Poly 1 R = Poly 1 R
132 eqid algSc Poly 1 R = algSc Poly 1 R
133 131 132 ply1ascl algSc Poly 1 R = algSc 1 𝑜 mPoly R
134 eqid Scalar 1 𝑜 mPoly R = Scalar 1 𝑜 mPoly R
135 133 134 asclrhm 1 𝑜 mPoly R AssAlg algSc Poly 1 R Scalar 1 𝑜 mPoly R RingHom 1 𝑜 mPoly R
136 130 135 syl φ algSc Poly 1 R Scalar 1 𝑜 mPoly R RingHom 1 𝑜 mPoly R
137 127 a1i φ 1 𝑜 On
138 128 137 125 mplsca φ R = Scalar 1 𝑜 mPoly R
139 138 oveq1d φ R RingHom 1 𝑜 mPoly R = Scalar 1 𝑜 mPoly R RingHom 1 𝑜 mPoly R
140 136 139 eleqtrrd φ algSc Poly 1 R R RingHom 1 𝑜 mPoly R
141 eqid Base 1 𝑜 mPoly R = Base 1 𝑜 mPoly R
142 1 141 rhmf algSc Poly 1 R R RingHom 1 𝑜 mPoly R algSc Poly 1 R : B Base 1 𝑜 mPoly R
143 140 142 syl φ algSc Poly 1 R : B Base 1 𝑜 mPoly R
144 143 ffvelrnda φ a B algSc Poly 1 R a Base 1 𝑜 mPoly R
145 eqid eval 1 R = eval 1 R
146 145 34 1 128 141 evl1val R CRing algSc Poly 1 R a Base 1 𝑜 mPoly R eval 1 R algSc Poly 1 R a = 1 𝑜 eval R algSc Poly 1 R a w B 1 𝑜 × w
147 126 144 146 syl2anc φ a B eval 1 R algSc Poly 1 R a = 1 𝑜 eval R algSc Poly 1 R a w B 1 𝑜 × w
148 145 131 1 132 evl1sca R CRing a B eval 1 R algSc Poly 1 R a = B × a
149 125 148 sylan φ a B eval 1 R algSc Poly 1 R a = B × a
150 1 ressid R CRing R 𝑠 B = R
151 126 150 syl φ a B R 𝑠 B = R
152 151 oveq2d φ a B 1 𝑜 mPoly R 𝑠 B = 1 𝑜 mPoly R
153 152 fveq2d φ a B algSc 1 𝑜 mPoly R 𝑠 B = algSc 1 𝑜 mPoly R
154 153 133 eqtr4di φ a B algSc 1 𝑜 mPoly R 𝑠 B = algSc Poly 1 R
155 154 fveq1d φ a B algSc 1 𝑜 mPoly R 𝑠 B a = algSc Poly 1 R a
156 155 fveq2d φ a B 1 𝑜 eval R algSc 1 𝑜 mPoly R 𝑠 B a = 1 𝑜 eval R algSc Poly 1 R a
157 eqid 1 𝑜 mPoly R 𝑠 B = 1 𝑜 mPoly R 𝑠 B
158 eqid R 𝑠 B = R 𝑠 B
159 eqid algSc 1 𝑜 mPoly R 𝑠 B = algSc 1 𝑜 mPoly R 𝑠 B
160 127 a1i φ a B 1 𝑜 On
161 crngring R CRing R Ring
162 1 subrgid R Ring B SubRing R
163 125 161 162 3syl φ B SubRing R
164 163 adantr φ a B B SubRing R
165 simpr φ a B a B
166 35 157 158 1 159 160 126 164 165 evlssca φ a B 1 𝑜 eval R algSc 1 𝑜 mPoly R 𝑠 B a = B 1 𝑜 × a
167 156 166 eqtr3d φ a B 1 𝑜 eval R algSc Poly 1 R a = B 1 𝑜 × a
168 167 coeq1d φ a B 1 𝑜 eval R algSc Poly 1 R a w B 1 𝑜 × w = B 1 𝑜 × a w B 1 𝑜 × w
169 147 149 168 3eqtr3d φ a B B × a = B 1 𝑜 × a w B 1 𝑜 × w
170 snex f V
171 19 170 xpex B × f V
172 171 7 elab B × f x | ψ χ
173 14 172 sylibr φ f B B × f x | ψ
174 173 ralrimiva φ f B B × f x | ψ
175 sneq f = a f = a
176 175 xpeq2d f = a B × f = B × a
177 176 eleq1d f = a B × f x | ψ B × a x | ψ
178 177 rspccva f B B × f x | ψ a B B × a x | ψ
179 174 178 sylan φ a B B × a x | ψ
180 169 179 eqeltrrd φ a B B 1 𝑜 × a w B 1 𝑜 × w x | ψ
181 resiexg B V I B V
182 19 181 ax-mp I B V
183 182 8 elab I B x | ψ θ
184 15 183 sylibr φ I B x | ψ
185 27 184 eqeltrd φ b B 1 𝑜 b w B 1 𝑜 × w x | ψ
186 el1o a 1 𝑜 a =
187 fveq2 a = b a = b
188 186 187 sylbi a 1 𝑜 b a = b
189 188 mpteq2dv a 1 𝑜 b B 1 𝑜 b a = b B 1 𝑜 b
190 189 coeq1d a 1 𝑜 b B 1 𝑜 b a w B 1 𝑜 × w = b B 1 𝑜 b w B 1 𝑜 × w
191 190 eleq1d a 1 𝑜 b B 1 𝑜 b a w B 1 𝑜 × w x | ψ b B 1 𝑜 b w B 1 𝑜 × w x | ψ
192 185 191 syl5ibrcom φ a 1 𝑜 b B 1 𝑜 b a w B 1 𝑜 × w x | ψ
193 192 imp φ a 1 𝑜 b B 1 𝑜 b a w B 1 𝑜 × w x | ψ
194 4 1 38 pf1mpf A Q A b B 1 𝑜 b ran 1 𝑜 eval R
195 16 194 syl φ A b B 1 𝑜 b ran 1 𝑜 eval R
196 1 2 3 36 87 109 111 113 115 117 119 121 123 180 193 195 mpfind φ A b B 1 𝑜 b w B 1 𝑜 × w x | ψ
197 33 196 eqeltrrd φ A x | ψ
198 13 elabg A Q A x | ψ ρ
199 16 198 syl φ A x | ψ ρ
200 197 199 mpbid φ ρ