Metamath Proof Explorer

Theorem paddidm

Description: Projective subspace sum is idempotent. Part of Lemma 16.2 of MaedaMaeda p. 68. (Contributed by NM, 13-Jan-2012)

Ref Expression
Hypotheses paddidm.s ⊢ S = PSubSp ⁡ K
paddidm.p ⊢ + ˙ = + 𝑃 ⁡ K
Assertion paddidm ⊢ K ∈ B ∧ X ∈ S → X + ˙ X = X

Proof

Step Hyp Ref Expression
1 paddidm.s ⊢ S = PSubSp ⁡ K
2 paddidm.p ⊢ + ˙ = + 𝑃 ⁡ K
3 simpl ⊢ K ∈ B ∧ X ∈ S → K ∈ B
4 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
5 4 1 psubssat ⊢ K ∈ B ∧ X ∈ S → X ⊆ Atoms ⁡ K
6 eqid ⊢ ≤ K = ≤ K
7 eqid ⊢ join ⁡ K = join ⁡ K
8 6 7 4 2 elpadd ⊢ K ∈ B ∧ X ⊆ Atoms ⁡ K ∧ X ⊆ Atoms ⁡ K → p ∈ X + ˙ X ↔ p ∈ X ∨ p ∈ X ∨ p ∈ Atoms ⁡ K ∧ ∃ q ∈ X ∃ r ∈ X p ≤ K q join ⁡ K r
9 3 5 5 8 syl3anc ⊢ K ∈ B ∧ X ∈ S → p ∈ X + ˙ X ↔ p ∈ X ∨ p ∈ X ∨ p ∈ Atoms ⁡ K ∧ ∃ q ∈ X ∃ r ∈ X p ≤ K q join ⁡ K r
10 pm1.2 ⊢ p ∈ X ∨ p ∈ X → p ∈ X
11 10 a1i ⊢ K ∈ B ∧ X ∈ S → p ∈ X ∨ p ∈ X → p ∈ X
12 6 7 4 1 psubspi ⊢ K ∈ B ∧ X ∈ S ∧ p ∈ Atoms ⁡ K ∧ ∃ q ∈ X ∃ r ∈ X p ≤ K q join ⁡ K r → p ∈ X
13 12 3exp1 ⊢ K ∈ B → X ∈ S → p ∈ Atoms ⁡ K → ∃ q ∈ X ∃ r ∈ X p ≤ K q join ⁡ K r → p ∈ X
14 13 imp4b ⊢ K ∈ B ∧ X ∈ S → p ∈ Atoms ⁡ K ∧ ∃ q ∈ X ∃ r ∈ X p ≤ K q join ⁡ K r → p ∈ X
15 11 14 jaod ⊢ K ∈ B ∧ X ∈ S → p ∈ X ∨ p ∈ X ∨ p ∈ Atoms ⁡ K ∧ ∃ q ∈ X ∃ r ∈ X p ≤ K q join ⁡ K r → p ∈ X
16 9 15 sylbid ⊢ K ∈ B ∧ X ∈ S → p ∈ X + ˙ X → p ∈ X
17 16 ssrdv ⊢ K ∈ B ∧ X ∈ S → X + ˙ X ⊆ X
18 4 2 sspadd1 ⊢ K ∈ B ∧ X ⊆ Atoms ⁡ K ∧ X ⊆ Atoms ⁡ K → X ⊆ X + ˙ X
19 3 5 5 18 syl3anc ⊢ K ∈ B ∧ X ∈ S → X ⊆ X + ˙ X
20 17 19 eqssd ⊢ K ∈ B ∧ X ∈ S → X + ˙ X = X