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

Definition df-pj1 17289
 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 17287 . 2
2 vw . . 3
3 cvv 3045 . . 3
4 vt . . . 4
5 vu . . . 4
62cv 1443 . . . . . 6
7 cbs 15121 . . . . . 6
86, 7cfv 5582 . . . . 5
98cpw 3951 . . . 4
10 vz . . . . 5
114cv 1443 . . . . . 6
125cv 1443 . . . . . 6
13 clsm 17286 . . . . . . 7
146, 13cfv 5582 . . . . . 6
1511, 12, 14co 6290 . . . . 5
1610cv 1443 . . . . . . . 8
17 vx . . . . . . . . . 10
1817cv 1443 . . . . . . . . 9
19 vy . . . . . . . . . 10
2019cv 1443 . . . . . . . . 9
21 cplusg 15190 . . . . . . . . . 10
226, 21cfv 5582 . . . . . . . . 9
2318, 20, 22co 6290 . . . . . . . 8
2416, 23wceq 1444 . . . . . . 7
2524, 19, 12wrex 2738 . . . . . 6
2625, 17, 11crio 6251 . . . . 5
2710, 15, 26cmpt 4461 . . . 4
284, 5, 9, 9, 27cmpt2 6292 . . 3
292, 3, 28cmpt 4461 . 2
301, 29wceq 1444 1
 Colors of variables: wff setvar class This definition is referenced by:  pj1fval  17344
 Copyright terms: Public domain W3C validator