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

Metamath Proof Explorer

Theorem pj1rid

Description: The left projection function is the zero operator on the right subspace. (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 pj1rid ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 0 )

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 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
11 subgrcl ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐺 ∈ Grp )
13 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14 13 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
15 6 14 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
16 15 sselda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
17 13 1 3 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 0 + 𝑋 ) = 𝑋 )
18 12 16 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 0 + 𝑋 ) = 𝑋 )
19 18 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = ( 0 + 𝑋 ) )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
21 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑇 ∩ 𝑈 ) = { 0 } )
22 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
23 2 lsmub2 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) )
24 5 6 23 syl2anc ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) )
25 24 sselda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) )
26 3 subg0cl ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑇 )
27 10 26 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 0 ∈ 𝑇 )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
29 1 2 3 4 10 20 21 22 9 25 27 28 pj1eq ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 = ( 0 + 𝑋 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 0 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝑋 ) ) )
30 19 29 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 0 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝑋 ) )
31 30 simpld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 0 )