[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖(1 - P) • x‖ + ‖(1 - (1 - P)) • x‖
[PROOFSTEP]
rw [add_comm, sub_sub_cancel]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖
[PROOFSTEP]
exact h.Lnorm x
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ Commute P Q
[PROOFSTEP]
have PR_eq_RPR : ∀ R : M, IsLprojection X R → P * R = R * P * R := fun R h₃ => by
  --porting note: Needed to fix function, which changes indent of following linesrefine
    @eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
      rw [← norm_sub_eq_zero_iff]
      have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
        calc
          ‖R • x‖ =
              ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) :=
            by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
          _ =
              ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
                (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) :=
            by rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
          _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
            rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
          _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
          _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
            by
            rw [GE.ge]
            have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
            simpa only [mul_smul, sub_smul, one_smul] using this
      rw [GE.ge] at e1 
      nth_rewrite 2 [← add_zero ‖R • x‖] at e1 
      rw [add_le_add_iff_left, two_smul, ← two_mul] at e1 
      rw [le_antisymm_iff]
      refine' ⟨_, norm_nonneg _⟩
      rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
⊢ P * R = R * P * R
[PROOFSTEP]
refine
  @eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
    rw [← norm_sub_eq_zero_iff]
    have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
      calc
        ‖R • x‖ =
            ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) :=
          by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
        _ =
            ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) :=
          by rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
        _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
          rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
        _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
        _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
          by
          rw [GE.ge]
          have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
          simpa only [mul_smul, sub_smul, one_smul] using this
    rw [GE.ge] at e1 
    nth_rewrite 2 [← add_zero ‖R • x‖] at e1 
    rw [add_le_add_iff_left, two_smul, ← two_mul] at e1 
    rw [le_antisymm_iff]
    refine' ⟨_, norm_nonneg _⟩
    rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ (P * R) • x = (R * P * R) • x
[PROOFSTEP]
rw [← norm_sub_eq_zero_iff]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
  calc
    ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) :=
      by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
    _ =
        ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
          (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) :=
      by rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
    _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
      rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
    _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
    _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
      by
      rw [GE.ge]
      have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
      simpa only [mul_smul, sub_smul, one_smul] using this
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
[PROOFSTEP]
rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)
[PROOFSTEP]
rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
[PROOFSTEP]
rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
abel
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
abel
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖
[PROOFSTEP]
rw [GE.ge]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
this : ‖R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
simpa only [mul_smul, sub_smul, one_smul] using this
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
rw [GE.ge] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
nth_rewrite 2 [← add_zero ‖R • x‖] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖ + 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
rw [add_le_add_iff_left, two_smul, ← two_mul] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
rw [le_antisymm_iff]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0 ∧ 0 ≤ ‖(P * R) • x - (R * P * R) • x‖
[PROOFSTEP]
refine' ⟨_, norm_nonneg _⟩
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
[PROOFSTEP]
rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 2 * 0
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Commute P Q
[PROOFSTEP]
have QP_eq_QPQ : Q * P = Q * P * Q :=
  by
  have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
    calc
      P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
      _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
  rwa [eq_sub_iff_add_eq, add_right_eq_self, sub_eq_zero] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Q * P = Q * P * Q
[PROOFSTEP]
have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
  calc
    P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
    _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ P * (1 - Q) = (1 - Q) * P * (1 - Q)
[PROOFSTEP]
rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ (1 - Q) * P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
[PROOFSTEP]
noncomm_ring
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
⊢ Q * P = Q * P * Q
[PROOFSTEP]
rwa [eq_sub_iff_add_eq, add_right_eq_self, sub_eq_zero] at e1 
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ Commute P Q
[PROOFSTEP]
show P * Q = Q * P
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ P * Q = Q * P
[PROOFSTEP]
rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P * Q)
[PROOFSTEP]
refine' ⟨IsIdempotentElem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, _⟩
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ ∀ (x : X), ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
intro x
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
calc
  ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖ := by rw [add_sub_cancel'_right ((P * Q) • x) x]
  _ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ := by apply norm_add_le
  _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_smul, one_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖
[PROOFSTEP]
rw [add_sub_cancel'_right ((P * Q) • x) x]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x + (x - (P * Q) • x)‖ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
[PROOFSTEP]
apply norm_add_le
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
rw [sub_smul, one_smul]
[GOAL]
case refine'_2
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖
[PROOFSTEP]
calc
  ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖) := by
    rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
  _ ≥ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ :=
    ((add_le_add_iff_left ‖P • Q • x‖).mpr (norm_add_le (Q • x - P • Q • x) (x - Q • x)))
  _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
[PROOFSTEP]
rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P + Q - P * Q)
[PROOFSTEP]
convert (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1
[GOAL]
case h.e'_6
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)
[PROOFSTEP]
noncomm_ring
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P : { P // IsLprojection X P }
⊢ P ≤ P
[PROOFSTEP]
simpa only [coe_inf, ← sq] using P.prop.proj.eq.symm
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : P ≤ Q
h₂ : Q ≤ R
⊢ P ≤ R
[PROOFSTEP]
simp only [coe_inf] at h₁ h₂ ⊢
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P = ↑P * ↑R
[PROOFSTEP]
rw [h₁, mul_assoc, ← h₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
h₁ : P ≤ Q
h₂ : Q ≤ P
⊢ ↑P = ↑Q
[PROOFSTEP]
convert (P.prop.commute Q.prop).eq
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
⊢ IsIdempotentElem 0
[PROOFSTEP]
rw [IsIdempotentElem, zero_mul]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
x : X
⊢ ‖x‖ = ‖0 • x‖ + ‖(1 - 0) • x‖
[PROOFSTEP]
simp only [zero_smul, norm_zero, sub_zero, one_smul, zero_add]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : { P // IsLprojection X P }
Q : M
⊢ ↑Pᶜ * Q = Q - ↑P * Q
[PROOFSTEP]
rw [coe_compl, sub_mul, one_mul]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : { P // IsLprojection X P }
⊢ ↑P * ↑Pᶜ = 0
[PROOFSTEP]
rw [coe_compl, mul_sub, mul_one, P.prop.proj.eq, sub_self]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
[PROOFSTEP]
rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑Pᶜ)), ← mul_assoc (R : M) (↑Q * ↑R) _, ← coe_inf Q,
  (Pᶜ.prop.commute R.prop).eq, ((Q ⊓ R).prop.commute Pᶜ.prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
  mul_assoc (Q : M), ← mul_assoc, mul_assoc (R : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
  zero_add, add_zero, ← mul_assoc, P.prop.proj.eq, R.prop.proj.eq, ← coe_inf Q, mul_assoc,
  ((Q ⊓ R).prop.commute Pᶜ.prop).eq, ← mul_assoc, Pᶜ.prop.proj.eq]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ≤ P ⊔ Q
[PROOFSTEP]
rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq, sub_self, add_zero]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ Q ≤ P ⊔ Q
[PROOFSTEP]
rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq, ← mul_assoc, Q.prop.proj.eq,
  add_sub_cancel'_right]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ R → Q ≤ R → P ⊔ Q ≤ R
[PROOFSTEP]
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_sup, coe_inf, coe_sup, ← add_sub, add_mul, sub_mul, mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑R → ↑Q = ↑Q * ↑R → ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))
[PROOFSTEP]
intro h₁ h₂
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑R
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))
[PROOFSTEP]
rw [← h₂, ← h₁]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ⊓ Q ≤ P
[PROOFSTEP]
rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc, P.prop.proj.eq]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ⊓ Q ≤ Q
[PROOFSTEP]
rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ Q → P ≤ R → P ≤ Q ⊓ R
[PROOFSTEP]
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_inf, coe_inf, ← mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑Q → ↑P = ↑P * ↑R → ↑P = ↑P * ↑Q * ↑R
[PROOFSTEP]
intro h₁ h₂
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑P = ↑P * ↑R
⊢ ↑P = ↑P * ↑Q * ↑R
[PROOFSTEP]
rw [← h₁, ← h₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
[PROOFSTEP]
have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
  rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul, mul_add,
    (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
    zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq, mul_assoc,
    (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
[PROOFSTEP]
rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul, mul_add,
  (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
  zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq, mul_assoc,
  (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
[PROOFSTEP]
have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = (P : M) + ↑Q * ↑R * ↑Pᶜ := by
  rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, ← compl_mul,
    (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc, distrib_lattice_lemma, (Q.prop.commute R.prop).eq,
    distrib_lattice_lemma]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = ↑P + ↑Q * ↑R * ↑Pᶜ
[PROOFSTEP]
rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, ← compl_mul,
  (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc, distrib_lattice_lemma, (Q.prop.commute R.prop).eq,
  distrib_lattice_lemma]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
[PROOFSTEP]
rw [le_def, e₁, coe_inf, e₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
src✝² : HasCompl { f // IsLprojection X f } := hasCompl
src✝¹ : SDiff { P // IsLprojection X P } := sdiff
src✝ : BoundedOrder { P // IsLprojection X P } := boundedOrder
P : { P // IsLprojection X P }
⊢ ↑(P ⊓ Pᶜ) = ↑⊥
[PROOFSTEP]
rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
src✝² : HasCompl { f // IsLprojection X f } := hasCompl
src✝¹ : SDiff { P // IsLprojection X P } := sdiff
src✝ : BoundedOrder { P // IsLprojection X P } := boundedOrder
P : { P // IsLprojection X P }
⊢ ↑⊤ = ↑(P ⊔ Pᶜ)
[PROOFSTEP]
rw [coe_top, coe_sup, coe_compl, add_sub_cancel'_right, ← coe_compl, mul_compl_self, sub_zero]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
src✝² : HasCompl { f // IsLprojection X f } := hasCompl
src✝¹ : SDiff { P // IsLprojection X P } := sdiff
src✝ : BoundedOrder { P // IsLprojection X P } := boundedOrder
P Q : { P // IsLprojection X P }
⊢ ↑(P \ Q) = ↑(P ⊓ Qᶜ)
[PROOFSTEP]
rw [coe_sdiff, ← coe_compl, coe_inf]
