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 = w ∈ V ⟼ t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ ran ⁡ x ∈ t , y ∈ u ⟼ x + w y

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsm class LSSum
1 vw setvar w
2 cvv class V
3 vt setvar t
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 vu setvar u
9 vx setvar x
10 3 cv setvar t
11 vy setvar y
12 8 cv setvar u
13 9 cv setvar x
14 cplusg class + 𝑔
15 5 14 cfv class + w
16 11 cv setvar y
17 13 16 15 co class x + w y
18 9 11 10 12 17 cmpo class x ∈ t , y ∈ u ⟼ x + w y
19 18 crn class ran ⁡ x ∈ t , y ∈ u ⟼ x + w y
20 3 8 7 7 19 cmpo class t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ ran ⁡ x ∈ t , y ∈ u ⟼ x + w y
21 1 2 20 cmpt class w ∈ V ⟼ t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ ran ⁡ x ∈ t , y ∈ u ⟼ x + w y
22 0 21 wceq wff LSSum = w ∈ V ⟼ t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ ran ⁡ x ∈ t , y ∈ u ⟼ x + w y