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 ⊢ B = Base G
pj1fval.a ⊢ + ˙ = + G
pj1fval.s ⊢ ⊕ ˙ = LSSum ⁡ G
pj1fval.p ⊢ P = proj 1 ⁡ G
Assertion pj1val ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U → T P U ⁡ X = ι x ∈ T | ∃ y ∈ U X = x + ˙ y

Proof

Step Hyp Ref Expression
1 pj1fval.v ⊢ B = Base G
2 pj1fval.a ⊢ + ˙ = + G
3 pj1fval.s ⊢ ⊕ ˙ = LSSum ⁡ G
4 pj1fval.p ⊢ P = proj 1 ⁡ G
5 1 2 3 4 pj1fval ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B → T P U = z ∈ T ⊕ ˙ U ⟼ ι x ∈ T | ∃ y ∈ U z = x + ˙ y
6 5 adantr ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U → T P U = z ∈ T ⊕ ˙ U ⟼ ι x ∈ T | ∃ y ∈ U z = x + ˙ y
7 simpr ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U ∧ z = X → z = X
8 7 eqeq1d ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U ∧ z = X → z = x + ˙ y ↔ X = x + ˙ y
9 8 rexbidv ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U ∧ z = X → ∃ y ∈ U z = x + ˙ y ↔ ∃ y ∈ U X = x + ˙ y
10 9 riotabidv ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U ∧ z = X → ι x ∈ T | ∃ y ∈ U z = x + ˙ y = ι x ∈ T | ∃ y ∈ U X = x + ˙ y
11 simpr ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U → X ∈ T ⊕ ˙ U
12 riotaex ⊢ ι x ∈ T | ∃ y ∈ U X = x + ˙ y ∈ V
13 12 a1i ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U → ι x ∈ T | ∃ y ∈ U X = x + ˙ y ∈ V
14 6 10 11 13 fvmptd ⊢ G ∈ V ∧ T ⊆ B ∧ U ⊆ B ∧ X ∈ T ⊕ ˙ U → T P U ⁡ X = ι x ∈ T | ∃ y ∈ U X = x + ˙ y