Metamath Proof Explorer

Theorem pj1id

Description: Any element of a direct subspace sum can be decomposed into projections onto the left and right factors. (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses pj1eu.a 
|- .+ = ( +g ` G )
pj1eu.s 
|- .(+) = ( LSSum ` G )
pj1eu.o 
|- .0. = ( 0g ` G )
pj1eu.z 
|- Z = ( Cntz ` G )
pj1eu.2 
|- ( ph -> T e. ( SubGrp ` G ) )
pj1eu.3 
|- ( ph -> U e. ( SubGrp ` G ) )
pj1eu.4 
|- ( ph -> ( T i^i U ) = { .0. } )
pj1eu.5 
|- ( ph -> T C_ ( Z ` U ) )
pj1f.p 
|- P = ( proj1 ` G )
Assertion pj1id 
|- ( ( ph /\ X e. ( T .(+) U ) ) -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )

Proof

Step Hyp Ref Expression
1 pj1eu.a 
 |-  .+ = ( +g ` G )
2 pj1eu.s 
 |-  .(+) = ( LSSum ` G )
3 pj1eu.o 
 |-  .0. = ( 0g ` G )
4 pj1eu.z 
 |-  Z = ( Cntz ` G )
5 pj1eu.2 
 |-  ( ph -> T e. ( SubGrp ` G ) )
6 pj1eu.3 
 |-  ( ph -> U e. ( SubGrp ` G ) )
7 pj1eu.4 
 |-  ( ph -> ( T i^i U ) = { .0. } )
8 pj1eu.5 
 |-  ( ph -> T C_ ( Z ` U ) )
9 pj1f.p 
 |-  P = ( proj1 ` G )
10 subgrcl 
 |-  ( T e. ( SubGrp ` G ) -> G e. Grp )
11 5 10 syl 
 |-  ( ph -> G e. Grp )
12 eqid 
 |-  ( Base ` G ) = ( Base ` G )
13 12 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
14 5 13 syl 
 |-  ( ph -> T C_ ( Base ` G ) )
15 12 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
16 6 15 syl 
 |-  ( ph -> U C_ ( Base ` G ) )
17 11 14 16 3jca 
 |-  ( ph -> ( G e. Grp /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) )
18 12 1 2 9 pj1val 
 |-  ( ( ( G e. Grp /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) /\ X e. ( T .(+) U ) ) -> ( ( T P U ) ` X ) = ( iota_ x e. T E. y e. U X = ( x .+ y ) ) )
19 17 18 sylan 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> ( ( T P U ) ` X ) = ( iota_ x e. T E. y e. U X = ( x .+ y ) ) )
20 1 2 3 4 5 6 7 8 pj1eu 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> E! x e. T E. y e. U X = ( x .+ y ) )
21 riotacl2 
 |-  ( E! x e. T E. y e. U X = ( x .+ y ) -> ( iota_ x e. T E. y e. U X = ( x .+ y ) ) e. { x e. T | E. y e. U X = ( x .+ y ) } )
22 20 21 syl 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> ( iota_ x e. T E. y e. U X = ( x .+ y ) ) e. { x e. T | E. y e. U X = ( x .+ y ) } )
23 19 22 eqeltrd 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> ( ( T P U ) ` X ) e. { x e. T | E. y e. U X = ( x .+ y ) } )
24 oveq1 
 |-  ( x = ( ( T P U ) ` X ) -> ( x .+ y ) = ( ( ( T P U ) ` X ) .+ y ) )
25 24 eqeq2d 
 |-  ( x = ( ( T P U ) ` X ) -> ( X = ( x .+ y ) <-> X = ( ( ( T P U ) ` X ) .+ y ) ) )
26 25 rexbidv 
 |-  ( x = ( ( T P U ) ` X ) -> ( E. y e. U X = ( x .+ y ) <-> E. y e. U X = ( ( ( T P U ) ` X ) .+ y ) ) )
27 26 elrab 
 |-  ( ( ( T P U ) ` X ) e. { x e. T | E. y e. U X = ( x .+ y ) } <-> ( ( ( T P U ) ` X ) e. T /\ E. y e. U X = ( ( ( T P U ) ` X ) .+ y ) ) )
28 27 simprbi 
 |-  ( ( ( T P U ) ` X ) e. { x e. T | E. y e. U X = ( x .+ y ) } -> E. y e. U X = ( ( ( T P U ) ` X ) .+ y ) )
29 23 28 syl 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> E. y e. U X = ( ( ( T P U ) ` X ) .+ y ) )
30 simprr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> X = ( ( ( T P U ) ` X ) .+ y ) )
31 11 ad2antrr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> G e. Grp )
32 16 ad2antrr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> U C_ ( Base ` G ) )
33 14 ad2antrr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> T C_ ( Base ` G ) )
34 simplr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> X e. ( T .(+) U ) )
35 2 4 lsmcom2 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) )
36 5 6 8 35 syl3anc 
 |-  ( ph -> ( T .(+) U ) = ( U .(+) T ) )
37 36 ad2antrr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( T .(+) U ) = ( U .(+) T ) )
38 34 37 eleqtrd 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> X e. ( U .(+) T ) )
39 12 1 2 9 pj1val 
 |-  ( ( ( G e. Grp /\ U C_ ( Base ` G ) /\ T C_ ( Base ` G ) ) /\ X e. ( U .(+) T ) ) -> ( ( U P T ) ` X ) = ( iota_ u e. U E. v e. T X = ( u .+ v ) ) )
40 31 32 33 38 39 syl31anc 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( ( U P T ) ` X ) = ( iota_ u e. U E. v e. T X = ( u .+ v ) ) )
41 1 2 3 4 5 6 7 8 9 pj1f 
 |-  ( ph -> ( T P U ) : ( T .(+) U ) --> T )
42 41 ad2antrr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( T P U ) : ( T .(+) U ) --> T )
43 42 34 ffvelcdmd 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( ( T P U ) ` X ) e. T )
44 8 ad2antrr 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> T C_ ( Z ` U ) )
45 44 43 sseldd 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( ( T P U ) ` X ) e. ( Z ` U ) )
46 simprl 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> y e. U )
47 1 4 cntzi 
 |-  ( ( ( ( T P U ) ` X ) e. ( Z ` U ) /\ y e. U ) -> ( ( ( T P U ) ` X ) .+ y ) = ( y .+ ( ( T P U ) ` X ) ) )
48 45 46 47 syl2anc 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( ( ( T P U ) ` X ) .+ y ) = ( y .+ ( ( T P U ) ` X ) ) )
49 30 48 eqtrd 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> X = ( y .+ ( ( T P U ) ` X ) ) )
50 oveq2 
 |-  ( v = ( ( T P U ) ` X ) -> ( y .+ v ) = ( y .+ ( ( T P U ) ` X ) ) )
51 50 rspceeqv 
 |-  ( ( ( ( T P U ) ` X ) e. T /\ X = ( y .+ ( ( T P U ) ` X ) ) ) -> E. v e. T X = ( y .+ v ) )
52 43 49 51 syl2anc 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> E. v e. T X = ( y .+ v ) )
53 simpll 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ph )
54 incom 
 |-  ( U i^i T ) = ( T i^i U )
55 54 7 eqtrid 
 |-  ( ph -> ( U i^i T ) = { .0. } )
56 4 5 6 8 cntzrecd 
 |-  ( ph -> U C_ ( Z ` T ) )
57 1 2 3 4 6 5 55 56 pj1eu 
 |-  ( ( ph /\ X e. ( U .(+) T ) ) -> E! u e. U E. v e. T X = ( u .+ v ) )
58 53 38 57 syl2anc 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> E! u e. U E. v e. T X = ( u .+ v ) )
59 oveq1 
 |-  ( u = y -> ( u .+ v ) = ( y .+ v ) )
60 59 eqeq2d 
 |-  ( u = y -> ( X = ( u .+ v ) <-> X = ( y .+ v ) ) )
61 60 rexbidv 
 |-  ( u = y -> ( E. v e. T X = ( u .+ v ) <-> E. v e. T X = ( y .+ v ) ) )
62 61 riota2 
 |-  ( ( y e. U /\ E! u e. U E. v e. T X = ( u .+ v ) ) -> ( E. v e. T X = ( y .+ v ) <-> ( iota_ u e. U E. v e. T X = ( u .+ v ) ) = y ) )
63 46 58 62 syl2anc 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( E. v e. T X = ( y .+ v ) <-> ( iota_ u e. U E. v e. T X = ( u .+ v ) ) = y ) )
64 52 63 mpbid 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( iota_ u e. U E. v e. T X = ( u .+ v ) ) = y )
65 40 64 eqtrd 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( ( U P T ) ` X ) = y )
66 65 oveq2d 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) = ( ( ( T P U ) ` X ) .+ y ) )
67 30 66 eqtr4d 
 |-  ( ( ( ph /\ X e. ( T .(+) U ) ) /\ ( y e. U /\ X = ( ( ( T P U ) ` X ) .+ y ) ) ) -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )
68 29 67 rexlimddv 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )