This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
paddidm.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddidm ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 + 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 paddidm.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
2 paddidm.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 simpl ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → 𝐾 ∈ 𝐵 )
4 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
5 4 1 psubssat ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
6 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
8 6 7 4 2 elpadd ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ∈ ( 𝑋 + 𝑋 ) ↔ ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
9 3 5 5 8 syl3anc ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑝 ∈ ( 𝑋 + 𝑋 ) ↔ ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
10 pm1.2 ⊢ ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ 𝑋 )
11 10 a1i ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ 𝑋 ) )
12 6 7 4 1 psubspi ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑝 ∈ 𝑋 )
13 12 3exp1 ⊢ ( 𝐾 ∈ 𝐵 → ( 𝑋 ∈ 𝑆 → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → 𝑝 ∈ 𝑋 ) ) ) )
14 13 imp4b ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑝 ∈ 𝑋 ) )
15 11 14 jaod ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑝 ∈ 𝑋 ) )
16 9 15 sylbid ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑝 ∈ ( 𝑋 + 𝑋 ) → 𝑝 ∈ 𝑋 ) )
17 16 ssrdv ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 + 𝑋 ) ⊆ 𝑋 )
18 4 2 sspadd1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → 𝑋 ⊆ ( 𝑋 + 𝑋 ) )
19 3 5 5 18 syl3anc ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ ( 𝑋 + 𝑋 ) )
20 17 19 eqssd ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 + 𝑋 ) = 𝑋 )