This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pj1eq

Description: Any element of a direct subspace sum can be decomposed uniquely into projections onto the left and right factors. (Contributed by Mario Carneiro, 16-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 ) )
pj1f.p 
|- P = ( proj1 ` G )
pj1eq.5 
|- ( ph -> X e. ( T .(+) U ) )
pj1eq.6 
|- ( ph -> B e. T )
pj1eq.7 
|- ( ph -> C e. U )
Assertion pj1eq 
|- ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )

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 pj1eq.5 
 |-  ( ph -> X e. ( T .(+) U ) )
11 pj1eq.6 
 |-  ( ph -> B e. T )
12 pj1eq.7 
 |-  ( ph -> C e. U )
13 1 2 3 4 5 6 7 8 9 pj1id 
 |-  ( ( ph /\ X e. ( T .(+) U ) ) -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )
14 10 13 mpdan 
 |-  ( ph -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )
15 14 eqeq1d 
 |-  ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) = ( B .+ C ) ) )
16 1 2 3 4 5 6 7 8 9 pj1f 
 |-  ( ph -> ( T P U ) : ( T .(+) U ) --> T )
17 16 10 ffvelcdmd 
 |-  ( ph -> ( ( T P U ) ` X ) e. T )
18 1 2 3 4 5 6 7 8 9 pj2f 
 |-  ( ph -> ( U P T ) : ( T .(+) U ) --> U )
19 18 10 ffvelcdmd 
 |-  ( ph -> ( ( U P T ) ` X ) e. U )
20 1 3 4 5 6 7 8 17 11 19 12 subgdisjb 
 |-  ( ph -> ( ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )
21 15 20 bitrd 
 |-  ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )