# Metamath Proof Explorer

## Theorem pj1fval

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}={\mathrm{Base}}_{{G}}$
pj1fval.a
pj1fval.s
pj1fval.p ${⊢}{P}={proj}_{1}\left({G}\right)$
Assertion pj1fval

### Proof

Step Hyp Ref Expression
1 pj1fval.v ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 pj1fval.a
3 pj1fval.s
4 pj1fval.p ${⊢}{P}={proj}_{1}\left({G}\right)$
5 elex ${⊢}{G}\in {V}\to {G}\in \mathrm{V}$
6 5 3ad2ant1 ${⊢}\left({G}\in {V}\wedge {T}\subseteq {B}\wedge {U}\subseteq {B}\right)\to {G}\in \mathrm{V}$
7 fveq2 ${⊢}{g}={G}\to {\mathrm{Base}}_{{g}}={\mathrm{Base}}_{{G}}$
8 7 1 syl6eqr ${⊢}{g}={G}\to {\mathrm{Base}}_{{g}}={B}$
9 8 pweqd ${⊢}{g}={G}\to 𝒫{\mathrm{Base}}_{{g}}=𝒫{B}$
10 fveq2 ${⊢}{g}={G}\to \mathrm{LSSum}\left({g}\right)=\mathrm{LSSum}\left({G}\right)$
11 10 3 syl6eqr
12 11 oveqd
13 fveq2 ${⊢}{g}={G}\to {+}_{{g}}={+}_{{G}}$
14 13 2 syl6eqr
15 14 oveqd
16 15 eqeq2d
17 16 rexbidv
18 17 riotabidv
19 12 18 mpteq12dv
20 9 9 19 mpoeq123dv
21 df-pj1 ${⊢}{proj}_{1}=\left({g}\in \mathrm{V}⟼\left({t}\in 𝒫{\mathrm{Base}}_{{g}},{u}\in 𝒫{\mathrm{Base}}_{{g}}⟼\left({z}\in \left({t}\mathrm{LSSum}\left({g}\right){u}\right)⟼\left(\iota {x}\in {t}|\exists {y}\in {u}\phantom{\rule{.4em}{0ex}}{z}={x}{+}_{{g}}{y}\right)\right)\right)\right)$
22 1 fvexi ${⊢}{B}\in \mathrm{V}$
23 22 pwex ${⊢}𝒫{B}\in \mathrm{V}$
24 23 23 mpoex
25 20 21 24 fvmpt
26 6 25 syl
27 4 26 syl5eq
28 oveq12
30 simprl ${⊢}\left(\left({G}\in {V}\wedge {T}\subseteq {B}\wedge {U}\subseteq {B}\right)\wedge \left({t}={T}\wedge {u}={U}\right)\right)\to {t}={T}$
31 simprr ${⊢}\left(\left({G}\in {V}\wedge {T}\subseteq {B}\wedge {U}\subseteq {B}\right)\wedge \left({t}={T}\wedge {u}={U}\right)\right)\to {u}={U}$
32 31 rexeqdv
33 30 32 riotaeqbidv
34 29 33 mpteq12dv
35 simp2 ${⊢}\left({G}\in {V}\wedge {T}\subseteq {B}\wedge {U}\subseteq {B}\right)\to {T}\subseteq {B}$
36 22 elpw2 ${⊢}{T}\in 𝒫{B}↔{T}\subseteq {B}$
37 35 36 sylibr ${⊢}\left({G}\in {V}\wedge {T}\subseteq {B}\wedge {U}\subseteq {B}\right)\to {T}\in 𝒫{B}$
38 simp3 ${⊢}\left({G}\in {V}\wedge {T}\subseteq {B}\wedge {U}\subseteq {B}\right)\to {U}\subseteq {B}$
39 22 elpw2 ${⊢}{U}\in 𝒫{B}↔{U}\subseteq {B}$
40 38 39 sylibr ${⊢}\left({G}\in {V}\wedge {T}\subseteq {B}\wedge {U}\subseteq {B}\right)\to {U}\in 𝒫{B}$
41 ovex
42 41 mptex
43 42 a1i
44 27 34 37 40 43 ovmpod