Metamath Proof Explorer

Theorem padd12N

Description: Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 paddass.a 
 |-  A = ( Atoms ` K )
2 paddass.p 
 |-  .+ = ( +P ` K )
3 hllat 
 |-  ( K e. HL -> K e. Lat )
4 3 adantr 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> K e. Lat )
5 simpr1 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> X C_ A )
6 simpr2 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Y C_ A )
7 1 2 paddcom 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( Y .+ X ) )
8 4 5 6 7 syl3anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ Y ) = ( Y .+ X ) )
9 8 oveq1d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ Z ) = ( ( Y .+ X ) .+ Z ) )
10 1 2 paddass 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
11 simpl 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> K e. HL )
12 simpr3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Z C_ A )
13 1 2 paddass 
 |-  ( ( K e. HL /\ ( Y C_ A /\ X C_ A /\ Z C_ A ) ) -> ( ( Y .+ X ) .+ Z ) = ( Y .+ ( X .+ Z ) ) )
14 11 6 5 12 13 syl13anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( Y .+ X ) .+ Z ) = ( Y .+ ( X .+ Z ) ) )
15 9 10 14 3eqtr3d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )