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 ) )