R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.109042
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.109558
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.110521
inst✝² : Semiring S
M : Type ?u.110527
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x).snd = 0 ↔
    ↑(prodEquivOfIsCompl p q h) (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x) ∈ p
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.109042
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.109558
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.110521
inst✝² : Semiring S
M : Type ?u.110527
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x).snd = 0 ↔ x ∈ p
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
no goals
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.109042
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.109558
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.110521
inst✝² : Semiring S
M : Type ?u.110527
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x).snd = 0 ↔
    ↑(prodEquivOfIsCompl p q h) (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x) ∈ p
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
  mem_left_iff_eq_zero_of_disjoint h.disjoint]