Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pj1 Structured version   Unicode version

Definition df-pj1 15271
 Description: Define the left projection function, which takes two subgroups with trivial intersection and returns a function mapping the elements of the subgroup sum to their projections onto . (The other projection function can be obtained by swapping the roles of and .) (Contributed by Mario Carneiro, 15-Oct-2015.)
Assertion
Ref Expression
df-pj1
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-pj1
StepHypRef Expression
1 cpj1 15269 . 2
2 vw . . 3
3 cvv 2956 . . 3
4 vt . . . 4
5 vu . . . 4
62cv 1651 . . . . . 6
7 cbs 13469 . . . . . 6
86, 7cfv 5454 . . . . 5
98cpw 3799 . . . 4
10 vz . . . . 5
114cv 1651 . . . . . 6
125cv 1651 . . . . . 6
13 clsm 15268 . . . . . . 7
146, 13cfv 5454 . . . . . 6
1511, 12, 14co 6081 . . . . 5
1610cv 1651 . . . . . . . 8
17 vx . . . . . . . . . 10
1817cv 1651 . . . . . . . . 9
19 vy . . . . . . . . . 10
2019cv 1651 . . . . . . . . 9
21 cplusg 13529 . . . . . . . . . 10
226, 21cfv 5454 . . . . . . . . 9
2318, 20, 22co 6081 . . . . . . . 8
2416, 23wceq 1652 . . . . . . 7
2524, 19, 12wrex 2706 . . . . . 6
2625, 17, 11crio 6542 . . . . 5
2710, 15, 26cmpt 4266 . . . 4
284, 5, 9, 9, 27cmpt2 6083 . . 3
292, 3, 28cmpt 4266 . 2
301, 29wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  pj1fval  15326
 Copyright terms: Public domain W3C validator