# Metamath Proof Explorer

## Theorem gsmsymgreqlem1

Description: Lemma 1 for gsmsymgreq . (Contributed by AV, 26-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s
`|- S = ( SymGrp ` N )`
gsmsymgrfix.b
`|- B = ( Base ` S )`
gsmsymgreq.z
`|- Z = ( SymGrp ` M )`
gsmsymgreq.p
`|- P = ( Base ` Z )`
gsmsymgreq.i
`|- I = ( N i^i M )`
Assertion gsmsymgreqlem1
`|- ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) -> ( ( S gsum ( X ++ <" C "> ) ) ` J ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` J ) ) )`

### Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s
` |-  S = ( SymGrp ` N )`
2 gsmsymgrfix.b
` |-  B = ( Base ` S )`
3 gsmsymgreq.z
` |-  Z = ( SymGrp ` M )`
4 gsmsymgreq.p
` |-  P = ( Base ` Z )`
5 gsmsymgreq.i
` |-  I = ( N i^i M )`
6 simpr
` |-  ( ( X e. Word B /\ C e. B ) -> C e. B )`
7 simpr
` |-  ( ( Y e. Word P /\ R e. P ) -> R e. P )`
8 6 7 anim12i
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) ) -> ( C e. B /\ R e. P ) )`
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( C e. B /\ R e. P ) )`
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( C e. B /\ R e. P ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( C e. B /\ R e. P ) )`
12 simpll3
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> J e. I )`
13 simpr
` |-  ( ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) -> ( C ` J ) = ( R ` J ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( C ` J ) = ( R ` J ) )`
15 simprl
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) )`
16 12 14 15 3jca
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( J e. I /\ ( C ` J ) = ( R ` J ) /\ A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) ) )`
17 1 2 3 4 5 fvcosymgeq
` |-  ( ( C e. B /\ R e. P ) -> ( ( J e. I /\ ( C ` J ) = ( R ` J ) /\ A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) ) -> ( ( ( S gsum X ) o. C ) ` J ) = ( ( ( Z gsum Y ) o. R ) ` J ) ) )`
18 11 16 17 sylc
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( ( ( S gsum X ) o. C ) ` J ) = ( ( ( Z gsum Y ) o. R ) ` J ) )`
19 simpl1
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> N e. Fin )`
20 simpr1l
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> X e. Word B )`
21 simpr1r
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> C e. B )`
22 19 20 21 3jca
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( N e. Fin /\ X e. Word B /\ C e. B ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( N e. Fin /\ X e. Word B /\ C e. B ) )`
24 1 2 gsumccatsymgsn
` |-  ( ( N e. Fin /\ X e. Word B /\ C e. B ) -> ( S gsum ( X ++ <" C "> ) ) = ( ( S gsum X ) o. C ) )`
25 23 24 syl
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( S gsum ( X ++ <" C "> ) ) = ( ( S gsum X ) o. C ) )`
26 25 fveq1d
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( ( S gsum ( X ++ <" C "> ) ) ` J ) = ( ( ( S gsum X ) o. C ) ` J ) )`
27 simpl2
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> M e. Fin )`
28 simpr2l
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> Y e. Word P )`
29 simpr2r
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> R e. P )`
30 27 28 29 3jca
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( M e. Fin /\ Y e. Word P /\ R e. P ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( M e. Fin /\ Y e. Word P /\ R e. P ) )`
` |-  ( ( M e. Fin /\ Y e. Word P /\ R e. P ) -> ( Z gsum ( Y ++ <" R "> ) ) = ( ( Z gsum Y ) o. R ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( Z gsum ( Y ++ <" R "> ) ) = ( ( Z gsum Y ) o. R ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( ( Z gsum ( Y ++ <" R "> ) ) ` J ) = ( ( ( Z gsum Y ) o. R ) ` J ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) ) -> ( ( S gsum ( X ++ <" C "> ) ) ` J ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` J ) )`
` |-  ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) -> ( ( S gsum ( X ++ <" C "> ) ) ` J ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` J ) ) )`