Metamath Proof Explorer

Theorem pclunN

Description: The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclun.a 
|- A = ( Atoms ` K )
pclun.p 
|- .+ = ( +P ` K )
pclun.c 
|- U = ( PCl ` K )
Assertion pclunN 
|- ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X u. Y ) ) = ( U ` ( X .+ Y ) ) )

Proof

Step Hyp Ref Expression
1 pclun.a 
 |-  A = ( Atoms ` K )
2 pclun.p 
 |-  .+ = ( +P ` K )
3 pclun.c 
 |-  U = ( PCl ` K )
4 simp1 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> K e. V )
5 1 2 paddunssN 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( X u. Y ) C_ ( X .+ Y ) )
6 1 2 paddssat 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )
7 1 3 pclssN 
 |-  ( ( K e. V /\ ( X u. Y ) C_ ( X .+ Y ) /\ ( X .+ Y ) C_ A ) -> ( U ` ( X u. Y ) ) C_ ( U ` ( X .+ Y ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X u. Y ) ) C_ ( U ` ( X .+ Y ) ) )
9 unss 
 |-  ( ( X C_ A /\ Y C_ A ) <-> ( X u. Y ) C_ A )
10 9 biimpi 
 |-  ( ( X C_ A /\ Y C_ A ) -> ( X u. Y ) C_ A )
11 10 3adant1 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( X u. Y ) C_ A )
12 1 3 pclssidN 
 |-  ( ( K e. V /\ ( X u. Y ) C_ A ) -> ( X u. Y ) C_ ( U ` ( X u. Y ) ) )
13 4 11 12 syl2anc 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( X u. Y ) C_ ( U ` ( X u. Y ) ) )
14 unss 
 |-  ( ( X C_ ( U ` ( X u. Y ) ) /\ Y C_ ( U ` ( X u. Y ) ) ) <-> ( X u. Y ) C_ ( U ` ( X u. Y ) ) )
15 13 14 sylibr 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( X C_ ( U ` ( X u. Y ) ) /\ Y C_ ( U ` ( X u. Y ) ) ) )
16 simp2 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> X C_ A )
17 simp3 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> Y C_ A )
18 eqid 
 |-  ( PSubSp ` K ) = ( PSubSp ` K )
19 1 18 3 pclclN 
 |-  ( ( K e. V /\ ( X u. Y ) C_ A ) -> ( U ` ( X u. Y ) ) e. ( PSubSp ` K ) )
20 4 11 19 syl2anc 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X u. Y ) ) e. ( PSubSp ` K ) )
21 1 18 2 paddss 
 |-  ( ( K e. V /\ ( X C_ A /\ Y C_ A /\ ( U ` ( X u. Y ) ) e. ( PSubSp ` K ) ) ) -> ( ( X C_ ( U ` ( X u. Y ) ) /\ Y C_ ( U ` ( X u. Y ) ) ) <-> ( X .+ Y ) C_ ( U ` ( X u. Y ) ) ) )
22 4 16 17 20 21 syl13anc 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( ( X C_ ( U ` ( X u. Y ) ) /\ Y C_ ( U ` ( X u. Y ) ) ) <-> ( X .+ Y ) C_ ( U ` ( X u. Y ) ) ) )
23 15 22 mpbid 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ ( U ` ( X u. Y ) ) )
24 1 18 psubssat 
 |-  ( ( K e. V /\ ( U ` ( X u. Y ) ) e. ( PSubSp ` K ) ) -> ( U ` ( X u. Y ) ) C_ A )
25 4 20 24 syl2anc 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X u. Y ) ) C_ A )
26 1 3 pclssN 
 |-  ( ( K e. V /\ ( X .+ Y ) C_ ( U ` ( X u. Y ) ) /\ ( U ` ( X u. Y ) ) C_ A ) -> ( U ` ( X .+ Y ) ) C_ ( U ` ( U ` ( X u. Y ) ) ) )
27 4 23 25 26 syl3anc 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X .+ Y ) ) C_ ( U ` ( U ` ( X u. Y ) ) ) )
28 18 3 pclidN 
 |-  ( ( K e. V /\ ( U ` ( X u. Y ) ) e. ( PSubSp ` K ) ) -> ( U ` ( U ` ( X u. Y ) ) ) = ( U ` ( X u. Y ) ) )
29 4 20 28 syl2anc 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( U ` ( X u. Y ) ) ) = ( U ` ( X u. Y ) ) )
30 27 29 sseqtrd 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X .+ Y ) ) C_ ( U ` ( X u. Y ) ) )
31 8 30 eqssd 
 |-  ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X u. Y ) ) = ( U ` ( X .+ Y ) ) )