Metamath Proof Explorer

Theorem gsumws4

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

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

Proof

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