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 ) )
9 8 3adant3 
 |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( C e. B /\ R e. P ) )
10 9 adantl 
 |-  ( ( ( 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 ) )
11 10 adantr 
 |-  ( ( ( ( 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 ) )
14 13 adantl 
 |-  ( ( ( ( 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 ) )
23 22 adantr 
 |-  ( ( ( ( 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 ) )
31 30 adantr 
 |-  ( ( ( ( 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 ) )
32 3 4 gsumccatsymgsn 
 |-  ( ( M e. Fin /\ Y e. Word P /\ R e. P ) -> ( Z gsum ( Y ++ <" R "> ) ) = ( ( Z gsum Y ) o. R ) )
33 31 32 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 ) ) ) -> ( Z gsum ( Y ++ <" R "> ) ) = ( ( Z gsum Y ) o. R ) )
34 33 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 ) ) ) -> ( ( Z gsum ( Y ++ <" R "> ) ) ` J ) = ( ( ( Z gsum Y ) o. R ) ` J ) )
35 18 26 34 3eqtr4d 
 |-  ( ( ( ( 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 ) )
36 35 ex 
 |-  ( ( ( 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 ) ) )