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 biimtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ) ) → ( ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) → 𝑥 = 𝑢 ) )
25 13 24 syl5 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ) ) → ( ( 𝑋 = ( 𝑥 + 𝑦 ) ∧ 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
26 25 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇 ) ) → ( ∃ 𝑦 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( 𝑋 = ( 𝑥 + 𝑦 ) ∧ 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
27 12 26 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇 ) ) → ( ( ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ∧ ∃ 𝑣 ∈ 𝑈 𝑋 = ( 𝑢 + 𝑣 ) ) → 𝑥 = 𝑢 ) )
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 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ∃! 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) )