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 ‘ 𝑤 ) 𝑦 ) ) ) )