R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ ⊤ ≤ LinearMap.range (↑(aeval f) p) ⊔ LinearMap.range (↑(aeval f) q)
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.range (↑(aeval f) p) ⊔ LinearMap.range (↑(aeval f) q) = ⊤
rw [eq_top_iff]
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
a✝ : v ∈ ⊤
⊢ v ∈ LinearMap.range (↑(aeval f) p) ⊔ LinearMap.range (↑(aeval f) q)
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ ⊤ ≤ LinearMap.range (↑(aeval f) p) ⊔ LinearMap.range (↑(aeval f) q)
intro v _
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
a✝ : v ∈ ⊤
⊢ ∃ y, y ∈ LinearMap.range (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ y + z = v
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
a✝ : v ∈ ⊤
⊢ v ∈ LinearMap.range (↑(aeval f) p) ⊔ LinearMap.range (↑(aeval f) q)
rw [Submodule.mem_sup]
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y, y ∈ LinearMap.range (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ y + z = v
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
a✝ : v ∈ ⊤
⊢ ∃ y, y ∈ LinearMap.range (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ y + z = v
rcases hpq with ⟨p', q', hpq'⟩
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (p * p')) v ∈ LinearMap.range (↑(aeval f) p) ∧
    ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ ↑(↑(aeval f) (p * p')) v + z = v
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y, y ∈ LinearMap.range (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ y + z = v
use aeval f (p * p') v
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ ↑(↑(aeval f) (p * p')) v + z = v
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (p * p')) v ∈ LinearMap.range (↑(aeval f) p) ∧
    ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ ↑(↑(aeval f) (p * p')) v + z = v
use LinearMap.mem_range.2 ⟨aeval f p' v, by simp only [LinearMap.mul_apply, aeval_mul]⟩
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (q * q')) v ∈ LinearMap.range (↑(aeval f) q) ∧ ↑(↑(aeval f) (p * p')) v + ↑(↑(aeval f) (q * q')) v = v
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ z, z ∈ LinearMap.range (↑(aeval f) q) ∧ ↑(↑(aeval f) (p * p')) v + z = v
use aeval f (q * q') v
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (p * p')) v + ↑(↑(aeval f) (q * q')) v = v
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (q * q')) v ∈ LinearMap.range (↑(aeval f) q) ∧ ↑(↑(aeval f) (p * p')) v + ↑(↑(aeval f) (q * q')) v = v
use LinearMap.mem_range.2 ⟨aeval f q' v, by simp only [LinearMap.mul_apply, aeval_mul]⟩
no goals
case intro.intro
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (p * p')) v + ↑(↑(aeval f) (q * q')) v = v
simpa only [mul_comm p p', mul_comm q q', aeval_one, aeval_add] using
  congr_arg (fun p : R[X] => aeval f p v) hpq'
no goals
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) p) (↑(↑(aeval f) p') v) = ↑(↑(aeval f) (p * p')) v
simp only [LinearMap.mul_apply, aeval_mul]
no goals
R : Type u
S : Type ?u.696957
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) q) (↑(↑(aeval f) q') v) = ↑(↑(aeval f) (q * q')) v
simp only [LinearMap.mul_apply, aeval_mul]