Description: The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | topgrpfn.w | ⊢ 𝑊 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } | |
Assertion | topgrpplusg | ⊢ ( + ∈ 𝑋 → + = ( +g ‘ 𝑊 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topgrpfn.w | ⊢ 𝑊 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } | |
2 | 1 | topgrpstr | ⊢ 𝑊 Struct 〈 1 , 9 〉 |
3 | plusgid | ⊢ +g = Slot ( +g ‘ ndx ) | |
4 | snsstp2 | ⊢ { 〈 ( +g ‘ ndx ) , + 〉 } ⊆ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } | |
5 | 4 1 | sseqtrri | ⊢ { 〈 ( +g ‘ ndx ) , + 〉 } ⊆ 𝑊 |
6 | 2 3 5 | strfv | ⊢ ( + ∈ 𝑋 → + = ( +g ‘ 𝑊 ) ) |