Metamath Proof Explorer

Theorem paddass

Description: Projective subspace sum is associative. Equation 16.2.1 of MaedaMaeda p. 68. In our version, the subspaces do not have to be nonempty. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddass.a 
|- A = ( Atoms ` K )
paddass.p 
|- .+ = ( +P ` K )
Assertion paddass 
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )

Proof

Step Hyp Ref Expression
1 paddass.a 
 |-  A = ( Atoms ` K )
2 paddass.p 
 |-  .+ = ( +P ` K )
3 simpl 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> K e. HL )
4 simpr3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Z C_ A )
5 simpr2 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Y C_ A )
6 simpr1 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> X C_ A )
7 1 2 paddasslem18 
 |-  ( ( K e. HL /\ ( Z C_ A /\ Y C_ A /\ X C_ A ) ) -> ( Z .+ ( Y .+ X ) ) C_ ( ( Z .+ Y ) .+ X ) )
8 3 4 5 6 7 syl13anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Z .+ ( Y .+ X ) ) C_ ( ( Z .+ Y ) .+ X ) )
9 hllat 
 |-  ( K e. HL -> K e. Lat )
10 1 2 paddcom 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( Y .+ X ) )
11 9 10 syl3an1 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( Y .+ X ) )
12 11 3adant3r3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ Y ) = ( Y .+ X ) )
13 12 oveq1d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ Z ) = ( ( Y .+ X ) .+ Z ) )
14 1 2 paddssat 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ A ) -> ( Y .+ X ) C_ A )
15 3 5 6 14 syl3anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Y .+ X ) C_ A )
16 1 2 paddcom 
 |-  ( ( K e. Lat /\ ( Y .+ X ) C_ A /\ Z C_ A ) -> ( ( Y .+ X ) .+ Z ) = ( Z .+ ( Y .+ X ) ) )
17 9 16 syl3an1 
 |-  ( ( K e. HL /\ ( Y .+ X ) C_ A /\ Z C_ A ) -> ( ( Y .+ X ) .+ Z ) = ( Z .+ ( Y .+ X ) ) )
18 3 15 4 17 syl3anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( Y .+ X ) .+ Z ) = ( Z .+ ( Y .+ X ) ) )
19 13 18 eqtrd 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ Z ) = ( Z .+ ( Y .+ X ) ) )
20 1 2 paddcom 
 |-  ( ( K e. Lat /\ Y C_ A /\ Z C_ A ) -> ( Y .+ Z ) = ( Z .+ Y ) )
21 9 20 syl3an1 
 |-  ( ( K e. HL /\ Y C_ A /\ Z C_ A ) -> ( Y .+ Z ) = ( Z .+ Y ) )
22 21 3adant3r1 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Y .+ Z ) = ( Z .+ Y ) )
23 22 oveq2d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Y .+ Z ) ) = ( X .+ ( Z .+ Y ) ) )
24 1 2 paddssat 
 |-  ( ( K e. HL /\ Z C_ A /\ Y C_ A ) -> ( Z .+ Y ) C_ A )
25 3 4 5 24 syl3anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Z .+ Y ) C_ A )
26 1 2 paddcom 
 |-  ( ( K e. Lat /\ X C_ A /\ ( Z .+ Y ) C_ A ) -> ( X .+ ( Z .+ Y ) ) = ( ( Z .+ Y ) .+ X ) )
27 9 26 syl3an1 
 |-  ( ( K e. HL /\ X C_ A /\ ( Z .+ Y ) C_ A ) -> ( X .+ ( Z .+ Y ) ) = ( ( Z .+ Y ) .+ X ) )
28 3 6 25 27 syl3anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Z .+ Y ) ) = ( ( Z .+ Y ) .+ X ) )
29 23 28 eqtrd 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Y .+ Z ) ) = ( ( Z .+ Y ) .+ X ) )
30 8 19 29 3sstr4d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ Z ) C_ ( X .+ ( Y .+ Z ) ) )
31 1 2 paddasslem18 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )
32 30 31 eqssd 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )