Metamath Proof Explorer

Theorem paddcom

Description: Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 padd0.a 
 |-  A = ( Atoms ` K )
2 padd0.p 
 |-  .+ = ( +P ` K )
3 uncom 
 |-  ( X u. Y ) = ( Y u. X )
4 3 a1i 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( X u. Y ) = ( Y u. X ) )
5 simpl1 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> K e. Lat )
6 simpl2 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> X C_ A )
7 simprl 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> q e. X )
8 6 7 sseldd 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> q e. A )
9 eqid 
 |-  ( Base ` K ) = ( Base ` K )
10 9 1 atbase 
 |-  ( q e. A -> q e. ( Base ` K ) )
11 8 10 syl 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> q e. ( Base ` K ) )
12 simpl3 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> Y C_ A )
13 simprr 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> r e. Y )
14 12 13 sseldd 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> r e. A )
15 9 1 atbase 
 |-  ( r e. A -> r e. ( Base ` K ) )
16 14 15 syl 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> r e. ( Base ` K ) )
17 eqid 
 |-  ( join ` K ) = ( join ` K )
18 9 17 latjcom 
 |-  ( ( K e. Lat /\ q e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> ( q ( join ` K ) r ) = ( r ( join ` K ) q ) )
19 5 11 16 18 syl3anc 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> ( q ( join ` K ) r ) = ( r ( join ` K ) q ) )
20 19 breq2d 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( q e. X /\ r e. Y ) ) -> ( p ( le ` K ) ( q ( join ` K ) r ) <-> p ( le ` K ) ( r ( join ` K ) q ) ) )
21 20 2rexbidva 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) <-> E. q e. X E. r e. Y p ( le ` K ) ( r ( join ` K ) q ) ) )
22 rexcom 
 |-  ( E. q e. X E. r e. Y p ( le ` K ) ( r ( join ` K ) q ) <-> E. r e. Y E. q e. X p ( le ` K ) ( r ( join ` K ) q ) )
23 21 22 bitrdi 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) <-> E. r e. Y E. q e. X p ( le ` K ) ( r ( join ` K ) q ) ) )
24 23 rabbidv 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } = { p e. A | E. r e. Y E. q e. X p ( le ` K ) ( r ( join ` K ) q ) } )
25 4 24 uneq12d 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) = ( ( Y u. X ) u. { p e. A | E. r e. Y E. q e. X p ( le ` K ) ( r ( join ` K ) q ) } ) )
26 eqid 
 |-  ( le ` K ) = ( le ` K )
27 26 17 1 2 paddval 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) )
28 26 17 1 2 paddval 
 |-  ( ( K e. Lat /\ Y C_ A /\ X C_ A ) -> ( Y .+ X ) = ( ( Y u. X ) u. { p e. A | E. r e. Y E. q e. X p ( le ` K ) ( r ( join ` K ) q ) } ) )
29 28 3com23 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( Y .+ X ) = ( ( Y u. X ) u. { p e. A | E. r e. Y E. q e. X p ( le ` K ) ( r ( join ` K ) q ) } ) )
30 25 27 29 3eqtr4d 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( Y .+ X ) )