Description: Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | deg1propd.b1 | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) ) | |
deg1propd.b2 | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) ) | ||
deg1propd.p | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) | ||
Assertion | deg1propd | ⊢ ( 𝜑 → ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑆 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deg1propd.b1 | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) ) | |
2 | deg1propd.b2 | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) ) | |
3 | deg1propd.p | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) | |
4 | 1 2 3 | mdegpropd | ⊢ ( 𝜑 → ( 1o mDeg 𝑅 ) = ( 1o mDeg 𝑆 ) ) |
5 | eqid | ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 ) | |
6 | 5 | deg1fval | ⊢ ( deg1 ‘ 𝑅 ) = ( 1o mDeg 𝑅 ) |
7 | eqid | ⊢ ( deg1 ‘ 𝑆 ) = ( deg1 ‘ 𝑆 ) | |
8 | 7 | deg1fval | ⊢ ( deg1 ‘ 𝑆 ) = ( 1o mDeg 𝑆 ) |
9 | 4 6 8 | 3eqtr4g | ⊢ ( 𝜑 → ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑆 ) ) |