R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.107426
R₃ : Type ?u.107429
M : Type ?u.107432
M₁ : Type u_3
M₂ : Type ?u.107438
Mₗ₁ : Type ?u.107441
Mₗ₁' : Type ?u.107444
Mₗ₂ : Type ?u.107447
Mₗ₂' : Type ?u.107450
K : Type ?u.107453
K₁ : Type ?u.107456
K₂ : Type ?u.107459
V : Type ?u.107462
V₁ : Type ?u.107465
V₂ : Type ?u.107468
n : Type ?u.107471
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
p : Submodule R₁ M₁
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑(↑B ↑x✝¹) ↑x✝ = 0 → ↑(↑B ↑x✝) ↑x✝¹ = 0
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.107426
R₃ : Type ?u.107429
M : Type ?u.107432
M₁ : Type u_3
M₂ : Type ?u.107438
Mₗ₁ : Type ?u.107441
Mₗ₁' : Type ?u.107444
Mₗ₂ : Type ?u.107447
Mₗ₂' : Type ?u.107450
K : Type ?u.107453
K₁ : Type ?u.107456
K₂ : Type ?u.107459
V : Type ?u.107462
V₁ : Type ?u.107465
V₂ : Type ?u.107468
n : Type ?u.107471
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
p : Submodule R₁ M₁
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑(↑(domRestrict₁₂ B p p) x✝¹) x✝ = 0 → ↑(↑(domRestrict₁₂ B p p) x✝) x✝¹ = 0
simp_rw [domRestrict₁₂_apply]
no goals
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.107426
R₃ : Type ?u.107429
M : Type ?u.107432
M₁ : Type u_3
M₂ : Type ?u.107438
Mₗ₁ : Type ?u.107441
Mₗ₁' : Type ?u.107444
Mₗ₂ : Type ?u.107447
Mₗ₂' : Type ?u.107450
K : Type ?u.107453
K₁ : Type ?u.107456
K₂ : Type ?u.107459
V : Type ?u.107462
V₁ : Type ?u.107465
V₂ : Type ?u.107468
n : Type ?u.107471
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
p : Submodule R₁ M₁
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑(↑B ↑x✝¹) ↑x✝ = 0 → ↑(↑B ↑x✝) ↑x✝¹ = 0
exact H _ _