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 𝐵 = ( Base ‘ 𝑅 )
pf1ind.cp + = ( +g𝑅 )
pf1ind.ct · = ( .r𝑅 )
pf1ind.cq 𝑄 = ran ( eval1𝑅 )
pf1ind.ad ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜁 )
pf1ind.mu ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜎 )
pf1ind.wa ( 𝑥 = ( 𝐵 × { 𝑓 } ) → ( 𝜓𝜒 ) )
pf1ind.wb ( 𝑥 = ( I ↾ 𝐵 ) → ( 𝜓𝜃 ) )
pf1ind.wc ( 𝑥 = 𝑓 → ( 𝜓𝜏 ) )
pf1ind.wd ( 𝑥 = 𝑔 → ( 𝜓𝜂 ) )
pf1ind.we ( 𝑥 = ( 𝑓f + 𝑔 ) → ( 𝜓𝜁 ) )
pf1ind.wf ( 𝑥 = ( 𝑓f · 𝑔 ) → ( 𝜓𝜎 ) )
pf1ind.wg ( 𝑥 = 𝐴 → ( 𝜓𝜌 ) )
pf1ind.co ( ( 𝜑𝑓𝐵 ) → 𝜒 )
pf1ind.pr ( 𝜑𝜃 )
pf1ind.a ( 𝜑𝐴𝑄 )
Assertion pf1ind ( 𝜑𝜌 )

Proof

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