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 
|- .+ = ( +P ` K )
Assertion paddidm 
|- ( ( K e. B /\ X e. S ) -> ( X .+ X ) = X )

Proof

Step Hyp Ref Expression
1 paddidm.s 
 |-  S = ( PSubSp ` K )
2 paddidm.p 
 |-  .+ = ( +P ` K )
3 simpl 
 |-  ( ( K e. B /\ X e. S ) -> K e. B )
4 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
5 4 1 psubssat 
 |-  ( ( K e. B /\ X e. S ) -> X C_ ( Atoms ` K ) )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 eqid 
 |-  ( join ` K ) = ( join ` K )
8 6 7 4 2 elpadd 
 |-  ( ( K e. B /\ X C_ ( Atoms ` K ) /\ X C_ ( Atoms ` K ) ) -> ( p e. ( X .+ X ) <-> ( ( p e. X \/ p e. X ) \/ ( p e. ( Atoms ` K ) /\ E. q e. X E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
9 3 5 5 8 syl3anc 
 |-  ( ( K e. B /\ X e. S ) -> ( p e. ( X .+ X ) <-> ( ( p e. X \/ p e. X ) \/ ( p e. ( Atoms ` K ) /\ E. q e. X E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
10 pm1.2 
 |-  ( ( p e. X \/ p e. X ) -> p e. X )
11 10 a1i 
 |-  ( ( K e. B /\ X e. S ) -> ( ( p e. X \/ p e. X ) -> p e. X ) )
12 6 7 4 1 psubspi 
 |-  ( ( ( K e. B /\ X e. S /\ p e. ( Atoms ` K ) ) /\ E. q e. X E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) -> p e. X )
13 12 3exp1 
 |-  ( K e. B -> ( X e. S -> ( p e. ( Atoms ` K ) -> ( E. q e. X E. r e. X p ( le ` K ) ( q ( join ` K ) r ) -> p e. X ) ) ) )
14 13 imp4b 
 |-  ( ( K e. B /\ X e. S ) -> ( ( p e. ( Atoms ` K ) /\ E. q e. X E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) -> p e. X ) )
15 11 14 jaod 
 |-  ( ( K e. B /\ X e. S ) -> ( ( ( p e. X \/ p e. X ) \/ ( p e. ( Atoms ` K ) /\ E. q e. X E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) ) -> p e. X ) )
16 9 15 sylbid 
 |-  ( ( K e. B /\ X e. S ) -> ( p e. ( X .+ X ) -> p e. X ) )
17 16 ssrdv 
 |-  ( ( K e. B /\ X e. S ) -> ( X .+ X ) C_ X )
18 4 2 sspadd1 
 |-  ( ( K e. B /\ X C_ ( Atoms ` K ) /\ X C_ ( Atoms ` K ) ) -> X C_ ( X .+ X ) )
19 3 5 5 18 syl3anc 
 |-  ( ( K e. B /\ X e. S ) -> X C_ ( X .+ X ) )
20 17 19 eqssd 
 |-  ( ( K e. B /\ X e. S ) -> ( X .+ X ) = X )