Metamath Proof Explorer

Theorem gsumws3

Description: Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020)

Ref Expression
Hypotheses gsumws3.0 
|- B = ( Base ` G )
gsumws3.1 
|- .+ = ( +g ` G )
Assertion gsumws3 
|- ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsum <" S T U "> ) = ( S .+ ( T .+ U ) ) )

Proof

Step Hyp Ref Expression
1 gsumws3.0 
 |-  B = ( Base ` G )
2 gsumws3.1 
 |-  .+ = ( +g ` G )
3 s1s2 
 |-  <" S T U "> = ( <" S "> ++ <" T U "> )
4 3 a1i 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> <" S T U "> = ( <" S "> ++ <" T U "> ) )
5 4 oveq2d 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsum <" S T U "> ) = ( G gsum ( <" S "> ++ <" T U "> ) ) )
6 simpl 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> G e. Mnd )
7 simprl 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> S e. B )
8 7 s1cld 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> <" S "> e. Word B )
9 simprrl 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> T e. B )
10 simprrr 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> U e. B )
11 9 10 s2cld 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> <" T U "> e. Word B )
12 1 2 gsumccat 
 |-  ( ( G e. Mnd /\ <" S "> e. Word B /\ <" T U "> e. Word B ) -> ( G gsum ( <" S "> ++ <" T U "> ) ) = ( ( G gsum <" S "> ) .+ ( G gsum <" T U "> ) ) )
13 6 8 11 12 syl3anc 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsum ( <" S "> ++ <" T U "> ) ) = ( ( G gsum <" S "> ) .+ ( G gsum <" T U "> ) ) )
14 1 gsumws1 
 |-  ( S e. B -> ( G gsum <" S "> ) = S )
15 14 ad2antrl 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsum <" S "> ) = S )
16 1 2 gsumws2 
 |-  ( ( G e. Mnd /\ T e. B /\ U e. B ) -> ( G gsum <" T U "> ) = ( T .+ U ) )
17 16 3expb 
 |-  ( ( G e. Mnd /\ ( T e. B /\ U e. B ) ) -> ( G gsum <" T U "> ) = ( T .+ U ) )
18 17 adantrl 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsum <" T U "> ) = ( T .+ U ) )
19 15 18 oveq12d 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( ( G gsum <" S "> ) .+ ( G gsum <" T U "> ) ) = ( S .+ ( T .+ U ) ) )
20 5 13 19 3eqtrd 
 |-  ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsum <" S T U "> ) = ( S .+ ( T .+ U ) ) )