Theorem pj1f

Description: The left projection function maps a direct subspace sum onto the left factor. (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	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
	pj1f.p	⊢ 𝑃 = ( proj1 ‘ 𝐺 )
Assertion	pj1f	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )

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	12 1 2 9	pj1fval	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 𝑃 𝑈 ) = ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) )
18	11 14 16 17	syl3anc	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) = ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) )
19	1 2 3 4 5 6 7 8	pj1eu	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ∃! 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) )
20		riotacl	⊢ ( ∃! 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) → ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ∈ 𝑇 )
21	19 20	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ∈ 𝑇 )
22	18 21	fmpt3d	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )