This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 = ( 𝐵 + 𝐶 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝐵 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝐶 ) ) )