Metamath Proof Explorer

Theorem rtelextdg2lem

Description: Lemma for rtelextdg2 : If an element X is a solution of a quadratic equation, then the degree of its field extension is at most 2. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses rtelextdg2.1 ⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
rtelextdg2.2 ⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
rtelextdg2.3 ⊢ 0 = ( 0g ‘ 𝐸 )
rtelextdg2.4 ⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
rtelextdg2.5 ⊢ 𝑉 = ( Base ‘ 𝐸 )
rtelextdg2.6 ⊢ · = ( .r ‘ 𝐸 )
rtelextdg2.7 ⊢ + = ( +g ‘ 𝐸 )
rtelextdg2.8 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐸 ) )
rtelextdg2.9 ⊢ ( 𝜑 → 𝐸 ∈ Field )
rtelextdg2.10 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
rtelextdg2.11 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
rtelextdg2.12 ⊢ ( 𝜑 → 𝐴 ∈ 𝐹 )
rtelextdg2.13 ⊢ ( 𝜑 → 𝐵 ∈ 𝐹 )
rtelextdg2.14 ⊢ ( 𝜑 → ( ( 2 ↑ 𝑋 ) + ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) = 0 )
rtelextdg2lem.1 ⊢ 𝑌 = ( var1 ‘ 𝐾 )
rtelextdg2lem.2 ⊢ ⊕ = ( +g ‘ 𝑃 )
rtelextdg2lem.3 ⊢ ⊗ = ( .r ‘ 𝑃 )
rtelextdg2lem.4 ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
rtelextdg2lem.5 ⊢ 𝑈 = ( algSc ‘ 𝑃 )
rtelextdg2lem.6 ⊢ 𝐺 = ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) )
Assertion rtelextdg2lem ( 𝜑 → ( 𝐿 [:] 𝐾 ) ≤ 2 )

Proof

Step Hyp Ref Expression
1 rtelextdg2.1 ⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
2 rtelextdg2.2 ⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
3 rtelextdg2.3 ⊢ 0 = ( 0g ‘ 𝐸 )
4 rtelextdg2.4 ⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
5 rtelextdg2.5 ⊢ 𝑉 = ( Base ‘ 𝐸 )
6 rtelextdg2.6 ⊢ · = ( .r ‘ 𝐸 )
7 rtelextdg2.7 ⊢ + = ( +g ‘ 𝐸 )
8 rtelextdg2.8 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐸 ) )
9 rtelextdg2.9 ⊢ ( 𝜑 → 𝐸 ∈ Field )
10 rtelextdg2.10 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
11 rtelextdg2.11 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 rtelextdg2.12 ⊢ ( 𝜑 → 𝐴 ∈ 𝐹 )
13 rtelextdg2.13 ⊢ ( 𝜑 → 𝐵 ∈ 𝐹 )
14 rtelextdg2.14 ⊢ ( 𝜑 → ( ( 2 ↑ 𝑋 ) + ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) = 0 )
15 rtelextdg2lem.1 ⊢ 𝑌 = ( var1 ‘ 𝐾 )
16 rtelextdg2lem.2 ⊢ ⊕ = ( +g ‘ 𝑃 )
17 rtelextdg2lem.3 ⊢ ⊗ = ( .r ‘ 𝑃 )
18 rtelextdg2lem.4 ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
19 rtelextdg2lem.5 ⊢ 𝑈 = ( algSc ‘ 𝑃 )
20 rtelextdg2lem.6 ⊢ 𝐺 = ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) )
21 eqid ⊢ ( deg1 ‘ 𝐸 ) = ( deg1 ‘ 𝐸 )
22 eqid ⊢ ( 𝐸 minPoly 𝐹 ) = ( 𝐸 minPoly 𝐹 )
23 fveq2 ⊢ ( 𝑝 = 𝐺 → ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝑝 ) = ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝐺 ) )
24 23 fveq1d ⊢ ( 𝑝 = 𝐺 → ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝑝 ) ‘ 𝑋 ) = ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝐺 ) ‘ 𝑋 ) )
25 24 eqeq1d ⊢ ( 𝑝 = 𝐺 → ( ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝑝 ) ‘ 𝑋 ) = 0 ↔ ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝐺 ) ‘ 𝑋 ) = 0 ) )
26 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
27 fldsdrgfld ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ) → ( 𝐸 ↾s 𝐹 ) ∈ Field )
28 9 10 27 syl2anc ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Field )
29 28 fldcrngd ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ CRing )
30 1 29 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ CRing )
31 30 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
32 4 ply1ring ⊢ ( 𝐾 ∈ Ring → 𝑃 ∈ Ring )
33 31 32 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
34 33 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
35 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
36 35 26 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
37 35 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
38 33 37 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
39 2nn0 ⊢ 2 ∈ ℕ0
40 39 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
41 15 4 26 vr1cl ⊢ ( 𝐾 ∈ Ring → 𝑌 ∈ ( Base ‘ 𝑃 ) )
42 31 41 syl ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑃 ) )
43 36 18 38 40 42 mulgnn0cld ⊢ ( 𝜑 → ( 2 ∧ 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
44 9 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
45 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
46 10 45 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
47 4 1 19 26 44 46 12 ressasclcl ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )
48 26 17 33 47 42 ringcld ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
49 4 1 19 26 44 46 13 ressasclcl ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐵 ) ∈ ( Base ‘ 𝑃 ) )
50 26 16 34 48 49 grpcld ⊢ ( 𝜑 → ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ∈ ( Base ‘ 𝑃 ) )
51 26 16 34 43 50 grpcld ⊢ ( 𝜑 → ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ∈ ( Base ‘ 𝑃 ) )
52 20 51 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝑃 ) )
53 20 fveq2i ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) )
54 53 fveq1i ⊢ ( ( coe1 ‘ 𝐺 ) ‘ 2 ) = ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 2 )
55 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
56 4 26 16 55 coe1addfv ⊢ ( ( ( 𝐾 ∈ Ring ∧ ( 2 ∧ 𝑌 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ∈ ( Base ‘ 𝑃 ) ) ∧ 2 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 2 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 2 ) ) )
57 31 43 50 40 56 syl31anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 2 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 2 ) ) )
58 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
59 eqid ⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
60 4 15 18 31 40 58 59 coe1mon ⊢ ( 𝜑 → ( coe1 ‘ ( 2 ∧ 𝑌 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 2 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) ) )
61 simpr ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → 𝑖 = 2 )
62 61 iftrued ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → if ( 𝑖 = 2 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 ) )
63 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ∈ V )
64 60 62 40 63 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 2 ) = ( 1r ‘ 𝐾 ) )
65 4 26 16 55 coe1addfv ⊢ ( ( ( 𝐾 ∈ Ring ∧ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑈 ‘ 𝐵 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 2 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 2 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 2 ) ) )
66 31 48 49 40 65 syl31anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 2 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 2 ) ) )
67 5 sdrgss ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ⊆ 𝑉 )
68 1 5 ressbas2 ⊢ ( 𝐹 ⊆ 𝑉 → 𝐹 = ( Base ‘ 𝐾 ) )
69 10 67 68 3syl ⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐾 ) )
70 12 69 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐾 ) )
71 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
72 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
73 4 26 71 19 17 72 coe1sclmulfv ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝐴 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) ∧ 2 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 2 ) = ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 2 ) ) )
74 31 70 42 40 73 syl121anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 2 ) = ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 2 ) ) )
75 4 15 31 58 59 coe1vr1 ⊢ ( 𝜑 → ( coe1 ‘ 𝑌 ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 1 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) ) )
76 1ne2 ⊢ 1 ≠ 2
77 76 nesymi ⊢ ¬ 2 = 1
78 eqeq1 ⊢ ( 𝑖 = 2 → ( 𝑖 = 1 ↔ 2 = 1 ) )
79 77 78 mtbiri ⊢ ( 𝑖 = 2 → ¬ 𝑖 = 1 )
80 79 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ¬ 𝑖 = 1 )
81 80 iffalsed ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → if ( 𝑖 = 1 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
82 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) ∈ V )
83 75 81 40 82 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝑌 ) ‘ 2 ) = ( 0g ‘ 𝐾 ) )
84 83 oveq2d ⊢ ( 𝜑 → ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 2 ) ) = ( 𝐴 ( .r ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) )
85 71 72 58 31 70 ringrzd ⊢ ( 𝜑 → ( 𝐴 ( .r ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
86 74 84 85 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 2 ) = ( 0g ‘ 𝐾 ) )
87 13 69 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ 𝐾 ) )
88 4 19 71 58 coe1scl ⊢ ( ( 𝐾 ∈ Ring ∧ 𝐵 ∈ ( Base ‘ 𝐾 ) ) → ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ 𝐾 ) ) ) )
89 31 87 88 syl2anc ⊢ ( 𝜑 → ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ 𝐾 ) ) ) )
90 0ne2 ⊢ 0 ≠ 2
91 90 neii ⊢ ¬ 0 = 2
92 eqeq1 ⊢ ( 𝑖 = 0 → ( 𝑖 = 2 ↔ 0 = 2 ) )
93 91 92 mtbiri ⊢ ( 𝑖 = 0 → ¬ 𝑖 = 2 )
94 93 61 nsyl3 ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ¬ 𝑖 = 0 )
95 94 iffalsed ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
96 89 95 40 82 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 2 ) = ( 0g ‘ 𝐾 ) )
97 86 96 oveq12d ⊢ ( 𝜑 → ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 2 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 2 ) ) = ( ( 0g ‘ 𝐾 ) ( +g ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) )
98 31 ringgrpd ⊢ ( 𝜑 → 𝐾 ∈ Grp )
99 71 58 grpidcl ⊢ ( 𝐾 ∈ Grp → ( 0g ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
100 98 99 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
101 71 55 58 98 100 grpridd ⊢ ( 𝜑 → ( ( 0g ‘ 𝐾 ) ( +g ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
102 66 97 101 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 2 ) = ( 0g ‘ 𝐾 ) )
103 64 102 oveq12d ⊢ ( 𝜑 → ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 2 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 2 ) ) = ( ( 1r ‘ 𝐾 ) ( +g ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) )
104 71 59 ringidcl ⊢ ( 𝐾 ∈ Ring → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
105 31 104 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
106 71 55 58 98 105 grpridd ⊢ ( 𝜑 → ( ( 1r ‘ 𝐾 ) ( +g ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 ) )
107 44 crngringd ⊢ ( 𝜑 → 𝐸 ∈ Ring )
108 eqid ⊢ ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐸 )
109 108 subrg1cl ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → ( 1r ‘ 𝐸 ) ∈ 𝐹 )
110 46 109 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) ∈ 𝐹 )
111 10 67 syl ⊢ ( 𝜑 → 𝐹 ⊆ 𝑉 )
112 1 5 108 ress1r ⊢ ( ( 𝐸 ∈ Ring ∧ ( 1r ‘ 𝐸 ) ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉 ) → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐾 ) )
113 107 110 111 112 syl3anc ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐾 ) )
114 106 113 eqtr4d ⊢ ( 𝜑 → ( ( 1r ‘ 𝐾 ) ( +g ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) = ( 1r ‘ 𝐸 ) )
115 57 103 114 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 2 ) = ( 1r ‘ 𝐸 ) )
116 54 115 eqtrid ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ 2 ) = ( 1r ‘ 𝐸 ) )
117 9 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
118 drngnzr ⊢ ( 𝐸 ∈ DivRing → 𝐸 ∈ NzRing )
119 108 3 nzrnz ⊢ ( 𝐸 ∈ NzRing → ( 1r ‘ 𝐸 ) ≠ 0 )
120 117 118 119 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) ≠ 0 )
121 116 120 eqnetrd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ 2 ) ≠ 0 )
122 fveq2 ⊢ ( 𝐺 = ( 0g ‘ 𝑃 ) → ( coe1 ‘ 𝐺 ) = ( coe1 ‘ ( 0g ‘ 𝑃 ) ) )
123 122 fveq1d ⊢ ( 𝐺 = ( 0g ‘ 𝑃 ) → ( ( coe1 ‘ 𝐺 ) ‘ 2 ) = ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 2 ) )
124 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
125 4 124 58 31 40 coe1zfv ⊢ ( 𝜑 → ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 2 ) = ( 0g ‘ 𝐾 ) )
126 107 ringgrpd ⊢ ( 𝜑 → 𝐸 ∈ Grp )
127 126 grpmndd ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
128 subrgsubg ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
129 46 128 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
130 3 subg0cl ⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → 0 ∈ 𝐹 )
131 129 130 syl ⊢ ( 𝜑 → 0 ∈ 𝐹 )
132 1 5 3 ress0g ⊢ ( ( 𝐸 ∈ Mnd ∧ 0 ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉 ) → 0 = ( 0g ‘ 𝐾 ) )
133 127 131 111 132 syl3anc ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐾 ) )
134 125 133 eqtr4d ⊢ ( 𝜑 → ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 2 ) = 0 )
135 123 134 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝐺 = ( 0g ‘ 𝑃 ) ) → ( ( coe1 ‘ 𝐺 ) ‘ 2 ) = 0 )
136 121 135 mteqand ⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
137 20 fveq2i ⊢ ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) = ( ( deg1 ‘ 𝐾 ) ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) )
138 eqid ⊢ ( deg1 ‘ 𝐾 ) = ( deg1 ‘ 𝐾 )
139 2re ⊢ 2 ∈ ℝ
140 139 rexri ⊢ 2 ∈ ℝ*
141 140 a1i ⊢ ( 𝜑 → 2 ∈ ℝ* )
142 138 4 26 deg1xrcl ⊢ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ∈ ( Base ‘ 𝑃 ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ∈ ℝ* )
143 48 142 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ∈ ℝ* )
144 1xr ⊢ 1 ∈ ℝ*
145 144 a1i ⊢ ( 𝜑 → 1 ∈ ℝ* )
146 138 4 71 26 17 19 deg1mul3le ⊢ ( ( 𝐾 ∈ Ring ∧ 𝐴 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ≤ ( ( deg1 ‘ 𝐾 ) ‘ 𝑌 ) )
147 31 70 42 146 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ≤ ( ( deg1 ‘ 𝐾 ) ‘ 𝑌 ) )
148 1 28 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ Field )
149 148 flddrngd ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
150 drngnzr ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ NzRing )
151 149 150 syl ⊢ ( 𝜑 → 𝐾 ∈ NzRing )
152 138 4 15 151 deg1vr ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ 𝑌 ) = 1 )
153 147 152 breqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ≤ 1 )
154 1lt2 ⊢ 1 < 2
155 154 a1i ⊢ ( 𝜑 → 1 < 2 )
156 143 145 141 153 155 xrlelttrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) < 2 )
157 138 4 26 deg1xrcl ⊢ ( ( 𝑈 ‘ 𝐵 ) ∈ ( Base ‘ 𝑃 ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑈 ‘ 𝐵 ) ) ∈ ℝ* )
158 49 157 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑈 ‘ 𝐵 ) ) ∈ ℝ* )
159 0xr ⊢ 0 ∈ ℝ*
160 159 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
161 138 4 71 19 deg1sclle ⊢ ( ( 𝐾 ∈ Ring ∧ 𝐵 ∈ ( Base ‘ 𝐾 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑈 ‘ 𝐵 ) ) ≤ 0 )
162 31 87 161 syl2anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑈 ‘ 𝐵 ) ) ≤ 0 )
163 2pos ⊢ 0 < 2
164 163 a1i ⊢ ( 𝜑 → 0 < 2 )
165 158 160 141 162 164 xrlelttrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑈 ‘ 𝐵 ) ) < 2 )
166 4 138 31 26 16 48 49 141 156 165 deg1addlt ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) < 2 )
167 138 4 15 35 18 deg1pw ⊢ ( ( 𝐾 ∈ NzRing ∧ 2 ∈ ℕ0 ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 2 ∧ 𝑌 ) ) = 2 )
168 151 40 167 syl2anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 2 ∧ 𝑌 ) ) = 2 )
169 166 168 breqtrrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 2 ∧ 𝑌 ) ) )
170 4 138 31 26 16 43 50 169 deg1add ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( 2 ∧ 𝑌 ) ) )
171 170 168 eqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) = 2 )
172 137 171 eqtrid ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) = 2 )
173 172 fveq2d ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) ) = ( ( coe1 ‘ 𝐺 ) ‘ 2 ) )
174 173 116 113 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) ) = ( 1r ‘ 𝐾 ) )
175 eqid ⊢ ( Monic1p ‘ 𝐾 ) = ( Monic1p ‘ 𝐾 )
176 4 26 124 138 175 59 ismon1p ⊢ ( 𝐺 ∈ ( Monic1p ‘ 𝐾 ) ↔ ( 𝐺 ∈ ( Base ‘ 𝑃 ) ∧ 𝐺 ≠ ( 0g ‘ 𝑃 ) ∧ ( ( coe1 ‘ 𝐺 ) ‘ ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) ) = ( 1r ‘ 𝐾 ) ) )
177 52 136 174 176 syl3anbrc ⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ 𝐾 ) )
178 eqid ⊢ ( 𝐸 evalSub1 𝐹 ) = ( 𝐸 evalSub1 𝐹 )
179 eqid ⊢ ( eval1 ‘ 𝐸 ) = ( eval1 ‘ 𝐸 )
180 178 5 4 1 26 179 44 46 ressply1evl ⊢ ( 𝜑 → ( 𝐸 evalSub1 𝐹 ) = ( ( eval1 ‘ 𝐸 ) ↾ ( Base ‘ 𝑃 ) ) )
181 180 fveq1d ⊢ ( 𝜑 → ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝐺 ) = ( ( ( eval1 ‘ 𝐸 ) ↾ ( Base ‘ 𝑃 ) ) ‘ 𝐺 ) )
182 52 fvresd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐸 ) ↾ ( Base ‘ 𝑃 ) ) ‘ 𝐺 ) = ( ( eval1 ‘ 𝐸 ) ‘ 𝐺 ) )
183 181 182 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝐺 ) = ( ( eval1 ‘ 𝐸 ) ‘ 𝐺 ) )
184 183 fveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝐺 ) ‘ 𝑋 ) = ( ( ( eval1 ‘ 𝐸 ) ‘ 𝐺 ) ‘ 𝑋 ) )
185 eqid ⊢ ( Poly1 ‘ 𝐸 ) = ( Poly1 ‘ 𝐸 )
186 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) = ( Base ‘ ( Poly1 ‘ 𝐸 ) )
187 eqid ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
188 eqid ⊢ ( ( coe1 ‘ 𝐺 ) ‘ 2 ) = ( ( coe1 ‘ 𝐺 ) ‘ 2 )
189 eqid ⊢ ( ( coe1 ‘ 𝐺 ) ‘ 1 ) = ( ( coe1 ‘ 𝐺 ) ‘ 1 )
190 eqid ⊢ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) = ( ( coe1 ‘ 𝐺 ) ‘ 0 )
191 eqid ⊢ ( PwSer1 ‘ 𝐾 ) = ( PwSer1 ‘ 𝐾 )
192 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) = ( Base ‘ ( PwSer1 ‘ 𝐾 ) )
193 185 1 4 26 46 191 192 186 ressply1bas2 ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ) )
194 52 193 eleqtrd ⊢ ( 𝜑 → 𝐺 ∈ ( ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ) )
195 194 elin2d ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) )
196 1 21 4 26 52 46 ressdeg1 ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐸 ) ‘ 𝐺 ) = ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) )
197 196 172 eqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐸 ) ‘ 𝐺 ) = 2 )
198 185 179 5 186 6 7 8 187 21 188 189 190 44 195 197 11 evl1deg2 ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐸 ) ‘ 𝐺 ) ‘ 𝑋 ) = ( ( ( ( coe1 ‘ 𝐺 ) ‘ 2 ) · ( 2 ↑ 𝑋 ) ) + ( ( ( ( coe1 ‘ 𝐺 ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ) )
199 116 oveq1d ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ 2 ) · ( 2 ↑ 𝑋 ) ) = ( ( 1r ‘ 𝐸 ) · ( 2 ↑ 𝑋 ) ) )
200 eqid ⊢ ( mulGrp ‘ 𝐸 ) = ( mulGrp ‘ 𝐸 )
201 200 5 mgpbas ⊢ 𝑉 = ( Base ‘ ( mulGrp ‘ 𝐸 ) )
202 200 ringmgp ⊢ ( 𝐸 ∈ Ring → ( mulGrp ‘ 𝐸 ) ∈ Mnd )
203 107 202 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐸 ) ∈ Mnd )
204 201 8 203 40 11 mulgnn0cld ⊢ ( 𝜑 → ( 2 ↑ 𝑋 ) ∈ 𝑉 )
205 5 6 108 107 204 ringlidmd ⊢ ( 𝜑 → ( ( 1r ‘ 𝐸 ) · ( 2 ↑ 𝑋 ) ) = ( 2 ↑ 𝑋 ) )
206 199 205 eqtrd ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ 2 ) · ( 2 ↑ 𝑋 ) ) = ( 2 ↑ 𝑋 ) )
207 53 fveq1i ⊢ ( ( coe1 ‘ 𝐺 ) ‘ 1 ) = ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 1 )
208 1nn0 ⊢ 1 ∈ ℕ0
209 208 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
210 4 26 16 55 coe1addfv ⊢ ( ( ( 𝐾 ∈ Ring ∧ ( 2 ∧ 𝑌 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ∈ ( Base ‘ 𝑃 ) ) ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 1 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 1 ) ) )
211 31 43 50 209 210 syl31anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 1 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 1 ) ) )
212 76 neii ⊢ ¬ 1 = 2
213 eqeq1 ⊢ ( 𝑖 = 1 → ( 𝑖 = 2 ↔ 1 = 2 ) )
214 213 notbid ⊢ ( 𝑖 = 1 → ( ¬ 𝑖 = 2 ↔ ¬ 1 = 2 ) )
215 214 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ¬ 𝑖 = 2 ↔ ¬ 1 = 2 ) )
216 212 215 mpbiri ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ¬ 𝑖 = 2 )
217 216 iffalsed ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → if ( 𝑖 = 2 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
218 60 217 209 82 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 1 ) = ( 0g ‘ 𝐾 ) )
219 4 26 16 55 coe1addfv ⊢ ( ( ( 𝐾 ∈ Ring ∧ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑈 ‘ 𝐵 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 1 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 1 ) ) )
220 31 48 49 209 219 syl31anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 1 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 1 ) ) )
221 4 26 71 19 17 72 coe1sclmulfv ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝐴 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 1 ) = ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 1 ) ) )
222 31 70 42 209 221 syl121anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 1 ) = ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 1 ) ) )
223 simpr ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → 𝑖 = 1 )
224 223 iftrued ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → if ( 𝑖 = 1 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 ) )
225 75 224 209 63 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝑌 ) ‘ 1 ) = ( 1r ‘ 𝐾 ) )
226 225 oveq2d ⊢ ( 𝜑 → ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 1 ) ) = ( 𝐴 ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) )
227 71 72 59 31 70 ringridmd ⊢ ( 𝜑 → ( 𝐴 ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) = 𝐴 )
228 222 226 227 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 1 ) = 𝐴 )
229 0ne1 ⊢ 0 ≠ 1
230 229 nesymi ⊢ ¬ 1 = 0
231 eqeq1 ⊢ ( 𝑖 = 1 → ( 𝑖 = 0 ↔ 1 = 0 ) )
232 230 231 mtbiri ⊢ ( 𝑖 = 1 → ¬ 𝑖 = 0 )
233 232 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ¬ 𝑖 = 0 )
234 233 iffalsed ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
235 89 234 209 82 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 1 ) = ( 0g ‘ 𝐾 ) )
236 228 235 oveq12d ⊢ ( 𝜑 → ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 1 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 1 ) ) = ( 𝐴 ( +g ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) )
237 71 55 58 98 70 grpridd ⊢ ( 𝜑 → ( 𝐴 ( +g ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) = 𝐴 )
238 220 236 237 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 1 ) = 𝐴 )
239 218 238 oveq12d ⊢ ( 𝜑 → ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 1 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 1 ) ) = ( ( 0g ‘ 𝐾 ) ( +g ‘ 𝐾 ) 𝐴 ) )
240 71 55 58 98 70 grplidd ⊢ ( 𝜑 → ( ( 0g ‘ 𝐾 ) ( +g ‘ 𝐾 ) 𝐴 ) = 𝐴 )
241 211 239 240 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 1 ) = 𝐴 )
242 207 241 eqtrid ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ 1 ) = 𝐴 )
243 242 oveq1d ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ 1 ) · 𝑋 ) = ( 𝐴 · 𝑋 ) )
244 53 fveq1i ⊢ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) = ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 0 )
245 0nn0 ⊢ 0 ∈ ℕ0
246 245 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
247 4 26 16 55 coe1addfv ⊢ ( ( ( 𝐾 ∈ Ring ∧ ( 2 ∧ 𝑌 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ∈ ( Base ‘ 𝑃 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 0 ) = ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 0 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 0 ) ) )
248 31 43 50 246 247 syl31anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 0 ) = ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 0 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 0 ) ) )
249 93 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ¬ 𝑖 = 2 )
250 249 iffalsed ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → if ( 𝑖 = 2 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
251 60 250 246 82 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 0 ) = ( 0g ‘ 𝐾 ) )
252 4 26 16 55 coe1addfv ⊢ ( ( ( 𝐾 ∈ Ring ∧ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑈 ‘ 𝐵 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 0 ) = ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 0 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 0 ) ) )
253 31 48 49 246 252 syl31anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 0 ) = ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 0 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 0 ) ) )
254 4 26 71 19 17 72 coe1sclmulfv ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝐴 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 0 ) = ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 0 ) ) )
255 31 70 42 246 254 syl121anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 0 ) = ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 0 ) ) )
256 229 neii ⊢ ¬ 0 = 1
257 eqeq1 ⊢ ( 𝑖 = 0 → ( 𝑖 = 1 ↔ 0 = 1 ) )
258 256 257 mtbiri ⊢ ( 𝑖 = 0 → ¬ 𝑖 = 1 )
259 258 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ¬ 𝑖 = 1 )
260 259 iffalsed ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → if ( 𝑖 = 1 , ( 1r ‘ 𝐾 ) , ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
261 75 260 246 82 fvmptd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝑌 ) ‘ 0 ) = ( 0g ‘ 𝐾 ) )
262 261 oveq2d ⊢ ( 𝜑 → ( 𝐴 ( .r ‘ 𝐾 ) ( ( coe1 ‘ 𝑌 ) ‘ 0 ) ) = ( 𝐴 ( .r ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) )
263 255 262 85 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 0 ) = ( 0g ‘ 𝐾 ) )
264 4 19 71 ply1sclid ⊢ ( ( 𝐾 ∈ Ring ∧ 𝐵 ∈ ( Base ‘ 𝐾 ) ) → 𝐵 = ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 0 ) )
265 31 87 264 syl2anc ⊢ ( 𝜑 → 𝐵 = ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 0 ) )
266 265 eqcomd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 0 ) = 𝐵 )
267 263 266 oveq12d ⊢ ( 𝜑 → ( ( ( coe1 ‘ ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ) ‘ 0 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( 𝑈 ‘ 𝐵 ) ) ‘ 0 ) ) = ( ( 0g ‘ 𝐾 ) ( +g ‘ 𝐾 ) 𝐵 ) )
268 71 55 58 98 87 grplidd ⊢ ( 𝜑 → ( ( 0g ‘ 𝐾 ) ( +g ‘ 𝐾 ) 𝐵 ) = 𝐵 )
269 253 267 268 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 0 ) = 𝐵 )
270 251 269 oveq12d ⊢ ( 𝜑 → ( ( ( coe1 ‘ ( 2 ∧ 𝑌 ) ) ‘ 0 ) ( +g ‘ 𝐾 ) ( ( coe1 ‘ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ‘ 0 ) ) = ( ( 0g ‘ 𝐾 ) ( +g ‘ 𝐾 ) 𝐵 ) )
271 248 270 268 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 2 ∧ 𝑌 ) ⊕ ( ( ( 𝑈 ‘ 𝐴 ) ⊗ 𝑌 ) ⊕ ( 𝑈 ‘ 𝐵 ) ) ) ) ‘ 0 ) = 𝐵 )
272 244 271 eqtrid ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ 0 ) = 𝐵 )
273 243 272 oveq12d ⊢ ( 𝜑 → ( ( ( ( coe1 ‘ 𝐺 ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
274 206 273 oveq12d ⊢ ( 𝜑 → ( ( ( ( coe1 ‘ 𝐺 ) ‘ 2 ) · ( 2 ↑ 𝑋 ) ) + ( ( ( ( coe1 ‘ 𝐺 ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ) = ( ( 2 ↑ 𝑋 ) + ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) )
275 274 14 eqtrd ⊢ ( 𝜑 → ( ( ( ( coe1 ‘ 𝐺 ) ‘ 2 ) · ( 2 ↑ 𝑋 ) ) + ( ( ( ( coe1 ‘ 𝐺 ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ) = 0 )
276 184 198 275 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝐺 ) ‘ 𝑋 ) = 0 )
277 25 177 276 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( Monic1p ‘ 𝐾 ) ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝑝 ) ‘ 𝑋 ) = 0 )
278 178 1 5 3 44 46 elirng ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐸 IntgRing 𝐹 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑝 ∈ ( Monic1p ‘ 𝐾 ) ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝑝 ) ‘ 𝑋 ) = 0 ) ) )
279 11 277 278 mpbir2and ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐸 IntgRing 𝐹 ) )
280 1 2 21 22 9 10 279 algextdeg ⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) = ( ( deg1 ‘ 𝐸 ) ‘ ( ( 𝐸 minPoly 𝐹 ) ‘ 𝑋 ) ) )
281 1 fveq2i ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
282 4 281 eqtri ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
283 eqid ⊢ { 𝑞 ∈ dom ( 𝐸 evalSub1 𝐹 ) ∣ ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝑞 ) ‘ 𝑋 ) = 0 } = { 𝑞 ∈ dom ( 𝐸 evalSub1 𝐹 ) ∣ ( ( ( 𝐸 evalSub1 𝐹 ) ‘ 𝑞 ) ‘ 𝑋 ) = 0 }
284 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
285 eqid ⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
286 178 282 5 9 10 11 3 283 284 285 22 minplycl ⊢ ( 𝜑 → ( ( 𝐸 minPoly 𝐹 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
287 1 21 4 26 286 46 ressdeg1 ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐸 ) ‘ ( ( 𝐸 minPoly 𝐹 ) ‘ 𝑋 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐸 minPoly 𝐹 ) ‘ 𝑋 ) ) )
288 280 287 eqtrd ⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) = ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐸 minPoly 𝐹 ) ‘ 𝑋 ) ) )
289 1 fveq2i ⊢ ( deg1 ‘ 𝐾 ) = ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) )
290 178 282 5 9 10 11 3 22 289 124 26 276 52 136 minplymindeg ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐸 minPoly 𝐹 ) ‘ 𝑋 ) ) ≤ ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) )
291 288 290 eqbrtrd ⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ≤ ( ( deg1 ‘ 𝐾 ) ‘ 𝐺 ) )
292 291 172 breqtrd ⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ≤ 2 )