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 ‘ 𝐺 )
pj1eu.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
pj1eu.o ⊢ 0 = ( 0g ‘ 𝐺 )
pj1eu.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
pj1eu.2 ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
pj1eu.3 ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
pj1eu.4 ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
pj1eu.5 ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
pj1f.p ⊢ 𝑃 = ( proj1 ‘ 𝐺 )
Assertion pj1id ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 pj1eu.a ⊢ + = ( +g ‘ 𝐺 )
2 pj1eu.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 pj1eu.o ⊢ 0 = ( 0g ‘ 𝐺 )
4 pj1eu.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
5 pj1eu.2 ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
6 pj1eu.3 ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
7 pj1eu.4 ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
8 pj1eu.5 ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
9 pj1f.p ⊢ 𝑃 = ( proj1 ‘ 𝐺 )
10 subgrcl ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
11 5 10 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
12 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13 12 subgss ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
14 5 13 syl ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
15 12 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
16 6 15 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
17 11 14 16 3jca ⊢ ( 𝜑 → ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) )
18 12 1 2 9 pj1val ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )
19 17 18 sylan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )
20 1 2 3 4 5 6 7 8 pj1eu ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ∃! 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) )
21 riotacl2 ⊢ ( ∃! 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) → ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) ∈ { 𝑥 ∈ 𝑇 ∣ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) } )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) ∈ { 𝑥 ∈ 𝑇 ∣ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) } )
23 19 22 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝑇 ∣ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) } )
24 oveq1 ⊢ ( 𝑥 = ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) → ( 𝑥 + 𝑦 ) = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) )
25 24 eqeq2d ⊢ ( 𝑥 = ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) → ( 𝑋 = ( 𝑥 + 𝑦 ) ↔ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) )
26 25 rexbidv ⊢ ( 𝑥 = ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑈 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) )
27 26 elrab ⊢ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝑇 ∣ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) } ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ 𝑇 ∧ ∃ 𝑦 ∈ 𝑈 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) )
28 27 simprbi ⊢ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝑇 ∣ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) } → ∃ 𝑦 ∈ 𝑈 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) )
29 23 28 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ∃ 𝑦 ∈ 𝑈 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) )
30 simprr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) )
31 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝐺 ∈ Grp )
32 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
33 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
34 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) )
35 2 4 lsmcom2 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
36 5 6 8 35 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
37 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
38 34 37 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑋 ∈ ( 𝑈 ⊕ 𝑇 ) )
39 12 1 2 9 pj1val ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑋 ∈ ( 𝑈 ⊕ 𝑇 ) ) → ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = ( ℩ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) ) )
40 31 32 33 38 39 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = ( ℩ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) ) )
41 1 2 3 4 5 6 7 8 9 pj1f ⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )
43 42 34 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ 𝑇 )
44 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
45 44 43 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ ( 𝑍 ‘ 𝑈 ) )
46 simprl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑦 ∈ 𝑈 )
47 1 4 cntzi ⊢ ( ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) = ( 𝑦 + ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ) )
48 45 46 47 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) = ( 𝑦 + ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ) )
49 30 48 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑋 = ( 𝑦 + ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ) )
50 oveq2 ⊢ ( 𝑣 = ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) → ( 𝑦 + 𝑣 ) = ( 𝑦 + ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ) )
51 50 rspceeqv ⊢ ( ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ 𝑇 ∧ 𝑋 = ( 𝑦 + ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ) ) → ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑦 + 𝑣 ) )
52 43 49 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑦 + 𝑣 ) )
53 simpll ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝜑 )
54 incom ⊢ ( 𝑈 ∩ 𝑇 ) = ( 𝑇 ∩ 𝑈 )
55 54 7 eqtrid ⊢ ( 𝜑 → ( 𝑈 ∩ 𝑇 ) = { 0 } )
56 4 5 6 8 cntzrecd ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) )
57 1 2 3 4 6 5 55 56 pj1eu ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑈 ⊕ 𝑇 ) ) → ∃! 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) )
58 53 38 57 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ∃! 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) )
59 oveq1 ⊢ ( 𝑢 = 𝑦 → ( 𝑢 + 𝑣 ) = ( 𝑦 + 𝑣 ) )
60 59 eqeq2d ⊢ ( 𝑢 = 𝑦 → ( 𝑋 = ( 𝑢 + 𝑣 ) ↔ 𝑋 = ( 𝑦 + 𝑣 ) ) )
61 60 rexbidv ⊢ ( 𝑢 = 𝑦 → ( ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) ↔ ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑦 + 𝑣 ) ) )
62 61 riota2 ⊢ ( ( 𝑦 ∈ 𝑈 ∧ ∃! 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) ) → ( ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑦 + 𝑣 ) ↔ ( ℩ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) ) = 𝑦 ) )
63 46 58 62 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑦 + 𝑣 ) ↔ ( ℩ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) ) = 𝑦 ) )
64 52 63 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ℩ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 𝑋 = ( 𝑢 + 𝑣 ) ) = 𝑦 )
65 40 64 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝑦 )
66 65 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) )
67 30 66 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) )
68 29 67 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) )