Theorem pj1eq

Description: Any element of a direct subspace sum can be decomposed uniquely into projections onto the left and right factors. (Contributed by Mario Carneiro, 16-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 ‘ 𝐺 )
	pj1eq.5	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) )
	pj1eq.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑇 )
	pj1eq.7	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
Assertion	pj1eq	⊢ ( 𝜑 → ( 𝑋 = ( 𝐵 + 𝐶 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝐵 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝐶 ) ) )

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		pj1eq.5	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) )
11		pj1eq.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑇 )
12		pj1eq.7	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
13	1 2 3 4 5 6 7 8 9	pj1id	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) )
14	10 13	mpdan	⊢ ( 𝜑 → 𝑋 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) )
15	14	eqeq1d	⊢ ( 𝜑 → ( 𝑋 = ( 𝐵 + 𝐶 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) = ( 𝐵 + 𝐶 ) ) )
16	1 2 3 4 5 6 7 8 9	pj1f	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )
17	16 10	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) ∈ 𝑇 )
18	1 2 3 4 5 6 7 8 9	pj2f	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑇 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑈 )
19	18 10	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ∈ 𝑈 )
20	1 3 4 5 6 7 8 17 11 19 12	subgdisjb	⊢ ( 𝜑 → ( ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) + ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) ) = ( 𝐵 + 𝐶 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝐵 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝐶 ) ) )
21	15 20	bitrd	⊢ ( 𝜑 → ( 𝑋 = ( 𝐵 + 𝐶 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝐵 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝐶 ) ) )