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