Description: The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | topgrpfn.w | |- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |
|
Assertion | topgrpplusg | |- ( .+ e. X -> .+ = ( +g ` W ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topgrpfn.w | |- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |
|
2 | 1 | topgrpstr | |- W Struct <. 1 , 9 >. |
3 | plusgid | |- +g = Slot ( +g ` ndx ) |
|
4 | snsstp2 | |- { <. ( +g ` ndx ) , .+ >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |
|
5 | 4 1 | sseqtrri | |- { <. ( +g ` ndx ) , .+ >. } C_ W |
6 | 2 3 5 | strfv | |- ( .+ e. X -> .+ = ( +g ` W ) ) |