Metamath Proof Explorer

Theorem mdegaddle

Description: The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y ⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
mdegaddle.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
mdegaddle.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mdegaddle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mdegaddle.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
mdegaddle.p ⊢ + = ( +g ‘ 𝑌 )
mdegaddle.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
mdegaddle.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion mdegaddle ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y ⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
2 mdegaddle.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
3 mdegaddle.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 mdegaddle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 mdegaddle.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
6 mdegaddle.p ⊢ + = ( +g ‘ 𝑌 )
7 mdegaddle.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8 mdegaddle.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
10 1 5 9 6 7 8 mpladd ⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) = ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) )
11 10 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ‘ 𝑐 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ‘ 𝑐 ) )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
15 1 13 5 14 7 mplelf ⊢ ( 𝜑 → 𝐹 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
16 15 ffnd ⊢ ( 𝜑 → 𝐹 Fn { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝐹 Fn { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
18 1 13 5 14 8 mplelf ⊢ ( 𝜑 → 𝐺 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
19 18 ffnd ⊢ ( 𝜑 → 𝐺 Fn { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝐺 Fn { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
21 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
22 21 rabex ⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∈ V
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∈ V )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
25 fnfvof ⊢ ( ( ( 𝐹 Fn { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ 𝐺 Fn { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ ( { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∈ V ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ) → ( ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ‘ 𝑐 ) = ( ( 𝐹 ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑐 ) ) )
26 17 20 23 24 25 syl22anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ‘ 𝑐 ) = ( ( 𝐹 ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑐 ) ) )
27 12 26 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( ( 𝐹 ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑐 ) ) )
28 27 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( ( 𝐹 ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑐 ) ) )
29 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
30 eqid ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
31 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → 𝐹 ∈ 𝐵 )
32 simprl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
33 2 1 5 mdegxrcl ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
34 7 33 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
36 2 1 5 mdegxrcl ⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
37 8 36 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
38 37 34 ifcld ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* )
40 nn0ssre ⊢ ℕ0 ⊆ ℝ
41 ressxr ⊢ ℝ ⊆ ℝ*
42 40 41 sstri ⊢ ℕ0 ⊆ ℝ*
43 14 30 tdeglem1 ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0
44 43 a1i ⊢ ( 𝜑 → ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 )
45 44 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℕ0 )
46 42 45 sselid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℝ* )
47 35 39 46 3jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℝ* ) )
48 47 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℝ* ) )
49 xrmax1 ⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ) → ( 𝐷 ‘ 𝐹 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
50 34 37 49 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( 𝐷 ‘ 𝐹 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
52 simprr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) )
53 51 52 jca ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐷 ‘ 𝐹 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) )
54 xrlelttr ⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℝ* ) → ( ( ( 𝐷 ‘ 𝐹 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) → ( 𝐷 ‘ 𝐹 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) )
55 48 53 54 sylc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( 𝐷 ‘ 𝐹 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) )
56 2 1 5 29 14 30 31 32 55 mdeglt ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( 𝐹 ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
57 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → 𝐺 ∈ 𝐵 )
58 37 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
59 58 39 46 3jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℝ* ) )
60 59 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℝ* ) )
61 xrmax2 ⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ) → ( 𝐷 ‘ 𝐺 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
62 34 37 61 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( 𝐷 ‘ 𝐺 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
64 63 52 jca ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐷 ‘ 𝐺 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) )
65 xrlelttr ⊢ ( ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ∈ ℝ* ) → ( ( ( 𝐷 ‘ 𝐺 ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) → ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) )
66 60 64 65 sylc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) )
67 2 1 5 29 14 30 57 32 66 mdeglt ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( 𝐺 ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
68 56 67 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐹 ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑐 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
69 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
70 4 69 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
71 13 29 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
72 4 71 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
73 13 9 29 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
74 70 72 73 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
76 68 75 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐹 ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑐 ) ) = ( 0g ‘ 𝑅 ) )
77 28 76 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) ) ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
78 77 expr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
79 78 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
80 1 3 4 mplringd ⊢ ( 𝜑 → 𝑌 ∈ Ring )
81 5 6 ringacl ⊢ ( ( 𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
82 80 7 8 81 syl3anc ⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
83 2 1 5 29 14 30 mdegleb ⊢ ( ( ( 𝐹 + 𝐺 ) ∈ 𝐵 ∧ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* ) → ( ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ↔ ∀ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
84 82 38 83 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ↔ ∀ 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑐 ) → ( ( 𝐹 + 𝐺 ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
85 79 84 mpbird ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )