no goals
R✝ : Type ?u.297453
inst✝¹⁴ : Ring R✝
E✝ : Type ?u.297459
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module R✝ E✝
F✝ : Type ?u.298018
inst✝¹¹ : AddCommGroup F✝
inst✝¹⁰ : Module R✝ F✝
G : Type ?u.298534
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module R✝ G
p✝ q✝ : Submodule R✝ E✝
S : Type ?u.299497
inst✝⁷ : Semiring S
M : Type ?u.299503
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module S M
m : Submodule S M
R : Type u_1
inst✝⁴ : CommRing R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
c : R
⊢ ∀ (u : { x // x ∈ p }), ↑(c • φ) u = ↑(c • ofIsCompl h φ ψ) ↑u
simp
no goals
R✝ : Type ?u.297453
inst✝¹⁴ : Ring R✝
E✝ : Type ?u.297459
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module R✝ E✝
F✝ : Type ?u.298018
inst✝¹¹ : AddCommGroup F✝
inst✝¹⁰ : Module R✝ F✝
G : Type ?u.298534
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module R✝ G
p✝ q✝ : Submodule R✝ E✝
S : Type ?u.299497
inst✝⁷ : Semiring S
M : Type ?u.299503
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module S M
m : Submodule S M
R : Type u_1
inst✝⁴ : CommRing R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
c : R
⊢ ∀ (u : { x // x ∈ q }), ↑(c • ψ) u = ↑(c • ofIsCompl h φ ψ) ↑u
simp