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	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 + 𝑋 ) = 𝑋 )