Metamath Proof Explorer

Theorem mulgaddcomlem

Description: Lemma for mulgaddcom . (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)

Ref Expression
Hypotheses mulgaddcom.b 
|- B = ( Base ` G )
mulgaddcom.t 
|- .x. = ( .g ` G )
mulgaddcom.p 
|- .+ = ( +g ` G )
Assertion mulgaddcomlem 
|- ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulgaddcom.b 
 |-  B = ( Base ` G )
2 mulgaddcom.t 
 |-  .x. = ( .g ` G )
3 mulgaddcom.p 
 |-  .+ = ( +g ` G )
4 simp1 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> G e. Grp )
5 4 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> G e. Grp )
6 simp3 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> X e. B )
7 6 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> X e. B )
8 znegcl 
 |-  ( y e. ZZ -> -u y e. ZZ )
9 1 2 mulgcl 
 |-  ( ( G e. Grp /\ -u y e. ZZ /\ X e. B ) -> ( -u y .x. X ) e. B )
10 8 9 syl3an2 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( -u y .x. X ) e. B )
11 10 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( -u y .x. X ) e. B )
12 eqid 
 |-  ( invg ` G ) = ( invg ` G )
13 1 12 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( invg ` G ) ` X ) e. B )
14 13 3adant2 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( ( invg ` G ) ` X ) e. B )
15 14 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( invg ` G ) ` X ) e. B )
16 1 3 grpass 
 |-  ( ( G e. Grp /\ ( X e. B /\ ( -u y .x. X ) e. B /\ ( ( invg ` G ) ` X ) e. B ) ) -> ( ( X .+ ( -u y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) = ( X .+ ( ( -u y .x. X ) .+ ( ( invg ` G ) ` X ) ) ) )
17 5 7 11 15 16 syl13anc 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( X .+ ( -u y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) = ( X .+ ( ( -u y .x. X ) .+ ( ( invg ` G ) ` X ) ) ) )
18 1 2 12 mulgneg 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( -u y .x. X ) = ( ( invg ` G ) ` ( y .x. X ) ) )
19 18 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( -u y .x. X ) = ( ( invg ` G ) ` ( y .x. X ) ) )
20 19 oveq1d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( -u y .x. X ) .+ ( ( invg ` G ) ` X ) ) = ( ( ( invg ` G ) ` ( y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) )
21 1 2 mulgcl 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( y .x. X ) e. B )
22 21 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( y .x. X ) e. B )
23 1 3 12 grpinvadd 
 |-  ( ( G e. Grp /\ X e. B /\ ( y .x. X ) e. B ) -> ( ( invg ` G ) ` ( X .+ ( y .x. X ) ) ) = ( ( ( invg ` G ) ` ( y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) )
24 5 7 22 23 syl3anc 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( invg ` G ) ` ( X .+ ( y .x. X ) ) ) = ( ( ( invg ` G ) ` ( y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) )
25 19 oveq2d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( ( invg ` G ) ` X ) .+ ( -u y .x. X ) ) = ( ( ( invg ` G ) ` X ) .+ ( ( invg ` G ) ` ( y .x. X ) ) ) )
26 1 3 12 grpinvadd 
 |-  ( ( G e. Grp /\ ( y .x. X ) e. B /\ X e. B ) -> ( ( invg ` G ) ` ( ( y .x. X ) .+ X ) ) = ( ( ( invg ` G ) ` X ) .+ ( ( invg ` G ) ` ( y .x. X ) ) ) )
27 5 22 7 26 syl3anc 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( invg ` G ) ` ( ( y .x. X ) .+ X ) ) = ( ( ( invg ` G ) ` X ) .+ ( ( invg ` G ) ` ( y .x. X ) ) ) )
28 fveq2 
 |-  ( ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) -> ( ( invg ` G ) ` ( ( y .x. X ) .+ X ) ) = ( ( invg ` G ) ` ( X .+ ( y .x. X ) ) ) )
29 28 adantl 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( invg ` G ) ` ( ( y .x. X ) .+ X ) ) = ( ( invg ` G ) ` ( X .+ ( y .x. X ) ) ) )
30 25 27 29 3eqtr2rd 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( invg ` G ) ` ( X .+ ( y .x. X ) ) ) = ( ( ( invg ` G ) ` X ) .+ ( -u y .x. X ) ) )
31 20 24 30 3eqtr2d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( -u y .x. X ) .+ ( ( invg ` G ) ` X ) ) = ( ( ( invg ` G ) ` X ) .+ ( -u y .x. X ) ) )
32 31 oveq2d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( X .+ ( ( -u y .x. X ) .+ ( ( invg ` G ) ` X ) ) ) = ( X .+ ( ( ( invg ` G ) ` X ) .+ ( -u y .x. X ) ) ) )
33 1 3 12 grpasscan1 
 |-  ( ( G e. Grp /\ X e. B /\ ( -u y .x. X ) e. B ) -> ( X .+ ( ( ( invg ` G ) ` X ) .+ ( -u y .x. X ) ) ) = ( -u y .x. X ) )
34 5 7 11 33 syl3anc 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( X .+ ( ( ( invg ` G ) ` X ) .+ ( -u y .x. X ) ) ) = ( -u y .x. X ) )
35 17 32 34 3eqtrd 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( X .+ ( -u y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) = ( -u y .x. X ) )
36 35 oveq1d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( ( X .+ ( -u y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) .+ X ) = ( ( -u y .x. X ) .+ X ) )
37 1 3 grpcl 
 |-  ( ( G e. Grp /\ X e. B /\ ( -u y .x. X ) e. B ) -> ( X .+ ( -u y .x. X ) ) e. B )
38 4 6 10 37 syl3anc 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( X .+ ( -u y .x. X ) ) e. B )
39 38 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( X .+ ( -u y .x. X ) ) e. B )
40 1 3 12 grpasscan2 
 |-  ( ( G e. Grp /\ ( X .+ ( -u y .x. X ) ) e. B /\ X e. B ) -> ( ( ( X .+ ( -u y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) .+ X ) = ( X .+ ( -u y .x. X ) ) )
41 5 39 7 40 syl3anc 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( ( X .+ ( -u y .x. X ) ) .+ ( ( invg ` G ) ` X ) ) .+ X ) = ( X .+ ( -u y .x. X ) ) )
42 36 41 eqtr3d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) )