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 = Base G
pj1fval.a + ˙ = + G
pj1fval.s ˙ = LSSum G
pj1fval.p P = proj 1 G
Assertion pj1fval G V T B U B T P U = z T ˙ U ι x T | y U z = 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 elex G V G V
6 5 3ad2ant1 G V T B U B G V
7 fveq2 g = G Base g = Base G
8 7 1 syl6eqr g = G Base g = B
9 8 pweqd g = G 𝒫 Base g = 𝒫 B
10 fveq2 g = G LSSum g = LSSum G
11 10 3 syl6eqr g = G LSSum g = ˙
12 11 oveqd g = G t LSSum g u = t ˙ u
13 fveq2 g = G + g = + G
14 13 2 syl6eqr g = G + g = + ˙
15 14 oveqd g = G x + g y = x + ˙ y
16 15 eqeq2d g = G z = x + g y z = x + ˙ y
17 16 rexbidv g = G y u z = x + g y y u z = x + ˙ y
18 17 riotabidv g = G ι x t | y u z = x + g y = ι x t | y u z = x + ˙ y
19 12 18 mpteq12dv g = G z t LSSum g u ι x t | y u z = x + g y = z t ˙ u ι x t | y u z = x + ˙ y
20 9 9 19 mpoeq123dv g = G t 𝒫 Base g , u 𝒫 Base g z t LSSum g u ι x t | y u z = x + g y = t 𝒫 B , u 𝒫 B z t ˙ u ι x t | y u z = x + ˙ y
21 df-pj1 proj 1 = g V t 𝒫 Base g , u 𝒫 Base g z t LSSum g u ι x t | y u z = x + g y
22 1 fvexi B V
23 22 pwex 𝒫 B V
24 23 23 mpoex t 𝒫 B , u 𝒫 B z t ˙ u ι x t | y u z = x + ˙ y V
25 20 21 24 fvmpt G V proj 1 G = t 𝒫 B , u 𝒫 B z t ˙ u ι x t | y u z = x + ˙ y
26 6 25 syl G V T B U B proj 1 G = t 𝒫 B , u 𝒫 B z t ˙ u ι x t | y u z = x + ˙ y
27 4 26 syl5eq G V T B U B P = t 𝒫 B , u 𝒫 B z t ˙ u ι x t | y u z = x + ˙ y
28 oveq12 t = T u = U t ˙ u = T ˙ U
29 28 adantl G V T B U B t = T u = U t ˙ u = T ˙ U
30 simprl G V T B U B t = T u = U t = T
31 simprr G V T B U B t = T u = U u = U
32 31 rexeqdv G V T B U B t = T u = U y u z = x + ˙ y y U z = x + ˙ y
33 30 32 riotaeqbidv G V T B U B t = T u = U ι x t | y u z = x + ˙ y = ι x T | y U z = x + ˙ y
34 29 33 mpteq12dv G V T B U B t = T u = U z t ˙ u ι x t | y u z = x + ˙ y = z T ˙ U ι x T | y U z = x + ˙ y
35 simp2 G V T B U B T B
36 22 elpw2 T 𝒫 B T B
37 35 36 sylibr G V T B U B T 𝒫 B
38 simp3 G V T B U B U B
39 22 elpw2 U 𝒫 B U B
40 38 39 sylibr G V T B U B U 𝒫 B
41 ovex T ˙ U V
42 41 mptex z T ˙ U ι x T | y U z = x + ˙ y V
43 42 a1i G V T B U B z T ˙ U ι x T | y U z = x + ˙ y V
44 27 34 37 40 43 ovmpod G V T B U B T P U = z T ˙ U ι x T | y U z = x + ˙ y