Metamath Proof Explorer


Theorem pj1eu

Description: Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015)

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 ( 𝜑𝑇 ⊆ ( 𝑍𝑈 ) )
Assertion pj1eu ( ( 𝜑𝑋 ∈ ( 𝑇 𝑈 ) ) → ∃! 𝑥𝑇𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) )

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 1 2 lsmelval ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑋 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑥𝑇𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )
10 5 6 9 syl2anc ( 𝜑 → ( 𝑋 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑥𝑇𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )
11 10 biimpa ( ( 𝜑𝑋 ∈ ( 𝑇 𝑈 ) ) → ∃ 𝑥𝑇𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) )
12 reeanv ( ∃ 𝑦𝑈𝑣𝑈 ( 𝑋 = ( 𝑥 + 𝑦 ) ∧ 𝑋 = ( 𝑢 + 𝑣 ) ) ↔ ( ∃ 𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ∧ ∃ 𝑣𝑈 𝑋 = ( 𝑢 + 𝑣 ) ) )
13 eqtr2 ( ( 𝑋 = ( 𝑥 + 𝑦 ) ∧ 𝑋 = ( 𝑢 + 𝑣 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) )
14 5 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
15 6 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
16 7 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → ( 𝑇𝑈 ) = { 0 } )
17 8 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → 𝑇 ⊆ ( 𝑍𝑈 ) )
18 simplrl ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → 𝑥𝑇 )
19 simplrr ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → 𝑢𝑇 )
20 simprl ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → 𝑦𝑈 )
21 simprr ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → 𝑣𝑈 )
22 1 3 4 14 15 16 17 18 19 20 21 subgdisjb ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → ( ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) ↔ ( 𝑥 = 𝑢𝑦 = 𝑣 ) ) )
23 simpl ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → 𝑥 = 𝑢 )
24 22 23 syl6bi ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → ( ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) → 𝑥 = 𝑢 ) )
25 13 24 syl5 ( ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) ∧ ( 𝑦𝑈𝑣𝑈 ) ) → ( ( 𝑋 = ( 𝑥 + 𝑦 ) ∧ 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
26 25 rexlimdvva ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) → ( ∃ 𝑦𝑈𝑣𝑈 ( 𝑋 = ( 𝑥 + 𝑦 ) ∧ 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
27 12 26 syl5bir ( ( 𝜑 ∧ ( 𝑥𝑇𝑢𝑇 ) ) → ( ( ∃ 𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ∧ ∃ 𝑣𝑈 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
28 27 ralrimivva ( 𝜑 → ∀ 𝑥𝑇𝑢𝑇 ( ( ∃ 𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ∧ ∃ 𝑣𝑈 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
29 28 adantr ( ( 𝜑𝑋 ∈ ( 𝑇 𝑈 ) ) → ∀ 𝑥𝑇𝑢𝑇 ( ( ∃ 𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ∧ ∃ 𝑣𝑈 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
30 oveq1 ( 𝑥 = 𝑢 → ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑦 ) )
31 30 eqeq2d ( 𝑥 = 𝑢 → ( 𝑋 = ( 𝑥 + 𝑦 ) ↔ 𝑋 = ( 𝑢 + 𝑦 ) ) )
32 31 rexbidv ( 𝑥 = 𝑢 → ( ∃ 𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ↔ ∃ 𝑦𝑈 𝑋 = ( 𝑢 + 𝑦 ) ) )
33 oveq2 ( 𝑦 = 𝑣 → ( 𝑢 + 𝑦 ) = ( 𝑢 + 𝑣 ) )
34 33 eqeq2d ( 𝑦 = 𝑣 → ( 𝑋 = ( 𝑢 + 𝑦 ) ↔ 𝑋 = ( 𝑢 + 𝑣 ) ) )
35 34 cbvrexvw ( ∃ 𝑦𝑈 𝑋 = ( 𝑢 + 𝑦 ) ↔ ∃ 𝑣𝑈 𝑋 = ( 𝑢 + 𝑣 ) )
36 32 35 bitrdi ( 𝑥 = 𝑢 → ( ∃ 𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ↔ ∃ 𝑣𝑈 𝑋 = ( 𝑢 + 𝑣 ) ) )
37 36 reu4 ( ∃! 𝑥𝑇𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ↔ ( ∃ 𝑥𝑇𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ∧ ∀ 𝑥𝑇𝑢𝑇 ( ( ∃ 𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) ∧ ∃ 𝑣𝑈 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) ) )
38 11 29 37 sylanbrc ( ( 𝜑𝑋 ∈ ( 𝑇 𝑈 ) ) → ∃! 𝑥𝑇𝑦𝑈 𝑋 = ( 𝑥 + 𝑦 ) )