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

Metamath Proof Explorer

Theorem pj1val

Description: The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

		Ref	Expression
	Hypotheses	pj1fval.v	⊢ 𝐵 = ( Base ‘ 𝐺 )
		pj1fval.a	⊢ + = ( +_g ‘ 𝐺 )
		pj1fval.s	⊢ ⊕ = ( LSSum ‘ 𝐺 )
		pj1fval.p	⊢ 𝑃 = ( proj₁ ‘ 𝐺 )
	Assertion	pj1val	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pj1fval.v	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		pj1fval.a	⊢ + = ( +_g ‘ 𝐺 )
3		pj1fval.s	⊢ ⊕ = ( LSSum ‘ 𝐺 )
4		pj1fval.p	⊢ 𝑃 = ( proj₁ ‘ 𝐺 )
5	1 2 3 4	pj1fval	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 𝑃 𝑈 ) = ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) )
6	5	adantr	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑇 𝑃 𝑈 ) = ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) )
7		simpr	⊢ ( ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ 𝑧 = 𝑋 ) → 𝑧 = 𝑋 )
8	7	eqeq1d	⊢ ( ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ 𝑧 = 𝑋 ) → ( 𝑧 = ( 𝑥 + 𝑦 ) ↔ 𝑋 = ( 𝑥 + 𝑦 ) ) )
9	8	rexbidv	⊢ ( ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ 𝑧 = 𝑋 ) → ( ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )
10	9	riotabidv	⊢ ( ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) ∧ 𝑧 = 𝑋 ) → ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) = ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )
11		simpr	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) )
12		riotaex	⊢ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) ∈ V
13	12	a1i	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) ∈ V )
14	6 10 11 13	fvmptd	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑥 + 𝑦 ) ) )