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

Metamath Proof Explorer

Theorem pj2f

Description: The right projection function maps a direct subspace sum onto the right 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 pj2f ( 𝜑 → ( 𝑈 𝑃 𝑇 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑈 )

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 incom ⊢ ( 𝑈 ∩ 𝑇 ) = ( 𝑇 ∩ 𝑈 )
11 10 7 eqtrid ⊢ ( 𝜑 → ( 𝑈 ∩ 𝑇 ) = { 0 } )
12 4 5 6 8 cntzrecd ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) )
13 1 2 3 4 6 5 11 12 9 pj1f ⊢ ( 𝜑 → ( 𝑈 𝑃 𝑇 ) : ( 𝑈 ⊕ 𝑇 ) ⟶ 𝑈 )
14 2 4 lsmcom2 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
15 5 6 8 14 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
16 15 feq2d ⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑇 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑈 ↔ ( 𝑈 𝑃 𝑇 ) : ( 𝑈 ⊕ 𝑇 ) ⟶ 𝑈 ) )
17 13 16 mpbird ⊢ ( 𝜑 → ( 𝑈 𝑃 𝑇 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑈 )