Metamath Proof Explorer

Theorem gsumws2

Description: Valuation of a pair in a monoid. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses gsumccat.b 
|- B = ( Base ` G )
gsumccat.p 
|- .+ = ( +g ` G )
Assertion gsumws2 
|- ( ( G e. Mnd /\ S e. B /\ T e. B ) -> ( G gsum <" S T "> ) = ( S .+ T ) )

Proof

Step Hyp Ref Expression
1 gsumccat.b 
 |-  B = ( Base ` G )
2 gsumccat.p 
 |-  .+ = ( +g ` G )
3 df-s2 
 |-  <" S T "> = ( <" S "> ++ <" T "> )
4 3 a1i 
 |-  ( ( G e. Mnd /\ S e. B /\ T e. B ) -> <" S T "> = ( <" S "> ++ <" T "> ) )
5 4 oveq2d 
 |-  ( ( G e. Mnd /\ S e. B /\ T e. B ) -> ( G gsum <" S T "> ) = ( G gsum ( <" S "> ++ <" T "> ) ) )
6 id 
 |-  ( G e. Mnd -> G e. Mnd )
7 s1cl 
 |-  ( S e. B -> <" S "> e. Word B )
8 s1cl 
 |-  ( T e. B -> <" T "> e. Word B )
9 1 2 gsumccat 
 |-  ( ( G e. Mnd /\ <" S "> e. Word B /\ <" T "> e. Word B ) -> ( G gsum ( <" S "> ++ <" T "> ) ) = ( ( G gsum <" S "> ) .+ ( G gsum <" T "> ) ) )
10 6 7 8 9 syl3an 
 |-  ( ( G e. Mnd /\ S e. B /\ T e. B ) -> ( G gsum ( <" S "> ++ <" T "> ) ) = ( ( G gsum <" S "> ) .+ ( G gsum <" T "> ) ) )
11 1 gsumws1 
 |-  ( S e. B -> ( G gsum <" S "> ) = S )
12 1 gsumws1 
 |-  ( T e. B -> ( G gsum <" T "> ) = T )
13 11 12 oveqan12d 
 |-  ( ( S e. B /\ T e. B ) -> ( ( G gsum <" S "> ) .+ ( G gsum <" T "> ) ) = ( S .+ T ) )
14 13 3adant1 
 |-  ( ( G e. Mnd /\ S e. B /\ T e. B ) -> ( ( G gsum <" S "> ) .+ ( G gsum <" T "> ) ) = ( S .+ T ) )
15 5 10 14 3eqtrd 
 |-  ( ( G e. Mnd /\ S e. B /\ T e. B ) -> ( G gsum <" S T "> ) = ( S .+ T ) )