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

Metamath Proof Explorer

Definition df-lsm

Description: Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014)

Ref Expression
Assertion df-lsm LSSum = ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsm ⊢ LSSum
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 vx ⊢ 𝑥
10 3 cv ⊢ 𝑡
11 vy ⊢ 𝑦
12 8 cv ⊢ 𝑢
13 9 cv ⊢ 𝑥
14 cplusg ⊢ +g
15 5 14 cfv ⊢ ( +g ‘ 𝑤 )
16 11 cv ⊢ 𝑦
17 13 16 15 co ⊢ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 )
18 9 11 10 12 17 cmpo ⊢ ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) )
19 18 crn ⊢ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) )
20 3 8 7 7 19 cmpo ⊢ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) )
21 1 2 20 cmpt ⊢ ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) )
22 0 21 wceq ⊢ LSSum = ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) )