This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-pj1

Description: Define the left projection function, which takes two subgroups t , u with trivial intersection and returns a function mapping the elements of the subgroup sum t + u to their projections onto t . (The other projection function can be obtained by swapping the roles of t and u .) (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion df-pj1 proj1 = ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpj1 ⊢ proj1
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vt ⊢ 𝑡
4 cbs ⊢ Base
5 1 cv ⊢ 𝑤
6 5 4 cfv ⊢ ( Base ‘ 𝑤 )
7 6 cpw ⊢ 𝒫 ( Base ‘ 𝑤 )
8 vu ⊢ 𝑢
9 vz ⊢ 𝑧
10 3 cv ⊢ 𝑡
11 clsm ⊢ LSSum
12 5 11 cfv ⊢ ( LSSum ‘ 𝑤 )
13 8 cv ⊢ 𝑢
14 10 13 12 co ⊢ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 )
15 vx ⊢ 𝑥
16 vy ⊢ 𝑦
17 9 cv ⊢ 𝑧
18 15 cv ⊢ 𝑥
19 cplusg ⊢ +g
20 5 19 cfv ⊢ ( +g ‘ 𝑤 )
21 16 cv ⊢ 𝑦
22 18 21 20 co ⊢ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 )
23 17 22 wceq ⊢ 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 )
24 23 16 13 wrex ⊢ ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 )
25 24 15 10 crio ⊢ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) )
26 9 14 25 cmpt ⊢ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) )
27 3 8 7 7 26 cmpo ⊢ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) )
28 1 2 27 cmpt ⊢ ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) ) )
29 0 28 wceq ⊢ proj1 = ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) ) )