Metamath Proof Explorer

Theorem pj1eu

Description: Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015)

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 ) )
Assertion pj1eu 
|- ( ( ph /\ X e. ( T .(+) U ) ) -> E! x e. T E. y e. U X = ( x .+ y ) )

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 1 2 lsmelval 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( X e. ( T .(+) U ) <-> E. x e. T E. y e. U X = ( x .+ y ) ) )
10 5 6 9 syl2anc 
 |-  ( ph -> ( X e. ( T .(+) U ) <-> E. x e. T E. y e. U X = ( x .+ y ) ) )
11 10 biimpa 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> E. x e. T E. y e. U X = ( x .+ y ) )
12 reeanv 
 |-  ( E. y e. U E. v e. U ( X = ( x .+ y ) /\ X = ( u .+ v ) ) <-> ( E. y e. U X = ( x .+ y ) /\ E. v e. U X = ( u .+ v ) ) )
13 eqtr2 
 |-  ( ( X = ( x .+ y ) /\ X = ( u .+ v ) ) -> ( x .+ y ) = ( u .+ v ) )
14 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> T e. ( SubGrp ` G ) )
15 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> U e. ( SubGrp ` G ) )
16 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> ( T i^i U ) = { .0. } )
17 8 ad2antrr 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> T C_ ( Z ` U ) )
18 simplrl 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> x e. T )
19 simplrr 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> u e. T )
20 simprl 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> y e. U )
21 simprr 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> v e. U )
22 1 3 4 14 15 16 17 18 19 20 21 subgdisjb 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> ( ( x .+ y ) = ( u .+ v ) <-> ( x = u /\ y = v ) ) )
23 simpl 
 |-  ( ( x = u /\ y = v ) -> x = u )
24 22 23 syl6bi 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> ( ( x .+ y ) = ( u .+ v ) -> x = u ) )
25 13 24 syl5 
 |-  ( ( ( ph /\ ( x e. T /\ u e. T ) ) /\ ( y e. U /\ v e. U ) ) -> ( ( X = ( x .+ y ) /\ X = ( u .+ v ) ) -> x = u ) )
26 25 rexlimdvva 
 |-  ( ( ph /\ ( x e. T /\ u e. T ) ) -> ( E. y e. U E. v e. U ( X = ( x .+ y ) /\ X = ( u .+ v ) ) -> x = u ) )
27 12 26 syl5bir 
 |-  ( ( ph /\ ( x e. T /\ u e. T ) ) -> ( ( E. y e. U X = ( x .+ y ) /\ E. v e. U X = ( u .+ v ) ) -> x = u ) )
28 27 ralrimivva 
 |-  ( ph -> A. x e. T A. u e. T ( ( E. y e. U X = ( x .+ y ) /\ E. v e. U X = ( u .+ v ) ) -> x = u ) )
29 28 adantr 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> A. x e. T A. u e. T ( ( E. y e. U X = ( x .+ y ) /\ E. v e. U X = ( u .+ v ) ) -> x = u ) )
30 oveq1 
 |-  ( x = u -> ( x .+ y ) = ( u .+ y ) )
31 30 eqeq2d 
 |-  ( x = u -> ( X = ( x .+ y ) <-> X = ( u .+ y ) ) )
32 31 rexbidv 
 |-  ( x = u -> ( E. y e. U X = ( x .+ y ) <-> E. y e. U X = ( u .+ y ) ) )
33 oveq2 
 |-  ( y = v -> ( u .+ y ) = ( u .+ v ) )
34 33 eqeq2d 
 |-  ( y = v -> ( X = ( u .+ y ) <-> X = ( u .+ v ) ) )
35 34 cbvrexvw 
 |-  ( E. y e. U X = ( u .+ y ) <-> E. v e. U X = ( u .+ v ) )
36 32 35 bitrdi 
 |-  ( x = u -> ( E. y e. U X = ( x .+ y ) <-> E. v e. U X = ( u .+ v ) ) )
37 36 reu4 
 |-  ( E! x e. T E. y e. U X = ( x .+ y ) <-> ( E. x e. T E. y e. U X = ( x .+ y ) /\ A. x e. T A. u e. T ( ( E. y e. U X = ( x .+ y ) /\ E. v e. U X = ( u .+ v ) ) -> x = u ) ) )
38 11 29 37 sylanbrc 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> E! x e. T E. y e. U X = ( x .+ y ) )