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 ffvelrnd ( ( ( 𝜑𝑋 ∈ ( 𝑇 𝑈 ) ) ∧ ( 𝑦𝑈𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + 𝑦 ) ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ 𝑇 )
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 syl5eq ( 𝜑 → ( 𝑈𝑇 ) = { 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 ( ( 𝜑𝑋 ∈ ( 𝑇 𝑈 ) ) → 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) )