MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpfind Unicode version

Theorem mpfind 21253
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, 19-Mar-2015.)
Hypotheses
Ref Expression
mpfind.cb
mpfind.cp
mpfind.ct
mpfind.cq
mpfind.ad
mpfind.mu
mpfind.wa
mpfind.wb
mpfind.wc
mpfind.wd
mpfind.we
mpfind.wf
mpfind.wg
mpfind.co
mpfind.pr
mpfind.a
Assertion
Ref Expression
mpfind
Distinct variable groups:   ,   ,   , ,   , ,   ,   ,   ,   ,   ,   ,   , , ,   ,I, ,   , , ,   Q, ,   , ,   S, ,   , , ,

Proof of Theorem mpfind
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpfind.a . . . . 5
2 mpfind.cq . . . . 5
31, 2syl6eleq 2512 . . . 4
42mpfrcl 21227 . . . . . . . . 9
51, 4syl 16 . . . . . . . 8
6 eqid 2422 . . . . . . . . 9
7 eqid 2422 . . . . . . . . 9
8 eqid 2422 . . . . . . . . 9
9 eqid 2422 . . . . . . . . 9
10 mpfind.cb . . . . . . . . 9
116, 7, 8, 9, 10evlsrhm 21230 . . . . . . . 8
125, 11syl 16 . . . . . . 7
13 eqid 2422 . . . . . . . 8
14 eqid 2422 . . . . . . . 8
1513, 14rhmf 16637 . . . . . . 7
1612, 15syl 16 . . . . . 6
17 ffn 5529 . . . . . 6
1816, 17syl 16 . . . . 5
19 fvelrnb 5709 . . . . 5
2018, 19syl 16 . . . 4
213, 20mpbid 204 . . 3
22 ffun 5531 . . . . . . . 8
2316, 22syl 16 . . . . . . 7
2423adantr 455 . . . . . 6
25 eqid 2422 . . . . . . 7
26 eqid 2422 . . . . . . 7
27 eqid 2422 . . . . . . 7
28 eqid 2422 . . . . . . 7
29 eqid 2422 . . . . . . 7
305simp1d 985 . . . . . . . . . . . 12
315simp2d 986 . . . . . . . . . . . . . 14
325simp3d 987 . . . . . . . . . . . . . 14
338subrgcrng 16682 . . . . . . . . . . . . . 14
3431, 32, 33syl2anc 646 . . . . . . . . . . . . 13
35 crngrng 16483 . . . . . . . . . . . . 13
3634, 35syl 16 . . . . . . . . . . . 12
377mplrng 17338 . . . . . . . . . . . 12
3830, 36, 37syl2anc 646 . . . . . . . . . . 11
3938adantr 455 . . . . . . . . . 10
40 simprl 740 . . . . . . . . . . . 12
41 elpreima 5793 . . . . . . . . . . . . . 14
4218, 41syl 16 . . . . . . . . . . . . 13
4342adantr 455 . . . . . . . . . . . 12
4440, 43mpbid 204 . . . . . . . . . . 11
4544simpld 449 . . . . . . . . . 10
46 simprr 741 . . . . . . . . . . . 12
47 elpreima 5793 . . . . . . . . . . . . . 14
4818, 47syl 16 . . . . . . . . . . . . 13
4948adantr 455 . . . . . . . . . . . 12
5046, 49mpbid 204 . . . . . . . . . . 11
5150simpld 449 . . . . . . . . . 10
5213, 27rngacl 16500 . . . . . . . . . 10
5339, 45, 51, 52syl3anc 1203 . . . . . . . . 9
54 rhmghm 16636 . . . . . . . . . . . . . 14
5512, 54syl 16 . . . . . . . . . . . . 13
5655adantr 455 . . . . . . . . . . . 12
57 eqid 2422 . . . . . . . . . . . . 13
5813, 27, 57ghmlin 15689 . . . . . . . . . . . 12
5956, 45, 51, 58syl3anc 1203 . . . . . . . . . . 11
6031adantr 455 . . . . . . . . . . . 12
61 ovex 6086 . . . . . . . . . . . . 13
6261a1i 11 . . . . . . . . . . . 12
6316adantr 455 . . . . . . . . . . . . 13
6463, 45ffvelrnd 5814 . . . . . . . . . . . 12
6563, 51ffvelrnd 5814 . . . . . . . . . . . 12
66 mpfind.cp . . . . . . . . . . . 12
679, 14, 60, 62, 64, 65, 66, 57pwsplusgval 14368 . . . . . . . . . . 11
6859, 67eqtrd 2454 . . . . . . . . . 10
69 simpl 447 . . . . . . . . . . 11
7018adantr 455 . . . . . . . . . . . . . 14
71 fnfvelrn 5810 . . . . . . . . . . . . . 14
7270, 45, 71syl2anc 646 . . . . . . . . . . . . 13
7372, 2syl6eleqr 2513 . . . . . . . . . . . 12
7423adantr 455 . . . . . . . . . . . . 13
75 fvimacnvi 5787 . . . . . . . . . . . . 13
7674, 40, 75syl2anc 646 . . . . . . . . . . . 12
7773, 76jca 522 . . . . . . . . . . 11
78 fnfvelrn 5810 . . . . . . . . . . . . . 14
7970, 51, 78syl2anc 646 . . . . . . . . . . . . 13
8079, 2syl6eleqr 2513 . . . . . . . . . . . 12
81 fvimacnvi 5787 . . . . . . . . . . . . 13
8274, 46, 81syl2anc 646 . . . . . . . . . . . 12
8380, 82jca 522 . . . . . . . . . . 11
84 fvex 5671 . . . . . . . . . . . 12
85 fvex 5671 . . . . . . . . . . . 12
86 eleq1 2482 . . . . . . . . . . . . . . . 16
87 vex 2954 . . . . . . . . . . . . . . . . . 18
88 mpfind.wc . . . . . . . . . . . . . . . . . 18
8987, 88elab 3084 . . . . . . . . . . . . . . . . 17
90 eleq1 2482 . . . . . . . . . . . . . . . . 17
9189, 90syl5bbr 253 . . . . . . . . . . . . . . . 16
9286, 91anbi12d 695 . . . . . . . . . . . . . . 15
93 eleq1 2482 . . . . . . . . . . . . . . . 16
94 vex 2954 . . . . . . . . . . . . . . . . . 18
95 mpfind.wd . . . . . . . . . . . . . . . . . 18
9694, 95elab 3084 . . . . . . . . . . . . . . . . 17
97 eleq1 2482 . . . . . . . . . . . . . . . . 17
9896, 97syl5bbr 253 . . . . . . . . . . . . . . . 16
9993, 98anbi12d 695 . . . . . . . . . . . . . . 15
10092, 99bi2anan9 853 . . . . . . . . . . . . . 14
101100anbi2d 688 . . . . . . . . . . . . 13
102 ovex 6086 . . . . . . . . . . . . . . 15
103 mpfind.we . . . . . . . . . . . . . . 15
104102, 103elab 3084 . . . . . . . . . . . . . 14
105 oveq12 6070 . . . . . . . . . . . . . . 15
106105eleq1d 2488 . . . . . . . . . . . . . 14
107104, 106syl5bbr 253 . . . . . . . . . . . . 13
108101, 107imbi12d 314 . . . . . . . . . . . 12
109 mpfind.ad . . . . . . . . . . . 12
11084, 85, 108, 109vtocl2 3003 . . . . . . . . . . 11
11169, 77, 83, 110syl12anc 1201 . . . . . . . . . 10
11268, 111eqeltrd 2496 . . . . . . . . 9
113 elpreima 5793 . . . . . . . . . . 11
11418, 113syl 16 . . . . . . . . . 10
115114adantr 455 . . . . . . . . 9
11653, 112, 115mpbir2and 898 . . . . . . . 8
117116adantlr 699 . . . . . . 7
11813, 28rngcl 16486 . . . . . . . . . 10
11939, 45, 51, 118syl3anc 1203 . . . . . . . . 9
120 eqid 2422 . . . . . . . . . . . . . . 15
121 eqid 2422 . . . . . . . . . . . . . . 15
122120, 121rhmmhm 16635 . . . . . . . . . . . . . 14
12312, 122syl 16 . . . . . . . . . . . . 13
124123adantr 455 . . . . . . . . . . . 12
125120, 13mgpbas 16463 . . . . . . . . . . . . 13
126120, 28mgpplusg 16461 . . . . . . . . . . . . 13
127 eqid 2422 . . . . . . . . . . . . . 14
128121, 127mgpplusg 16461 . . . . . . . . . . . . 13
129125, 126, 128mhmlin 15411