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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgaddcom.t ⊢ · = ( .g ‘ 𝐺 )
mulgaddcom.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulgaddcomlem ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgaddcom.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgaddcom.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgaddcom.p ⊢ + = ( +g ‘ 𝐺 )
4 simp1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝐺 ∈ Grp )
5 4 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → 𝐺 ∈ Grp )
6 simp3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7 6 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
8 znegcl ⊢ ( 𝑦 ∈ ℤ → - 𝑦 ∈ ℤ )
9 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑦 · 𝑋 ) ∈ 𝐵 )
10 8 9 syl3an2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑦 · 𝑋 ) ∈ 𝐵 )
11 10 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( - 𝑦 · 𝑋 ) ∈ 𝐵 )
12 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
13 1 12 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 )
14 13 3adant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 )
15 14 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 )
16 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ ( - 𝑦 · 𝑋 ) ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 ) ) → ( ( 𝑋 + ( - 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( 𝑋 + ( ( - 𝑦 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ) )
17 5 7 11 15 16 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( 𝑋 + ( - 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( 𝑋 + ( ( - 𝑦 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ) )
18 1 2 12 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑦 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) )
19 18 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( - 𝑦 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) )
20 19 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( - 𝑦 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) )
21 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
22 21 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
23 1 3 12 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑦 · 𝑋 ) ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) )
24 5 7 22 23 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) )
25 19 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( - 𝑦 · 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) ) )
26 1 3 12 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 · 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) ) )
27 5 22 7 26 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑦 · 𝑋 ) ) ) )
28 fveq2 ⊢ ( ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) )
29 28 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) )
30 25 27 29 3eqtr2rd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( - 𝑦 · 𝑋 ) ) )
31 20 24 30 3eqtr2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( - 𝑦 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( - 𝑦 · 𝑋 ) ) )
32 31 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( 𝑋 + ( ( - 𝑦 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ) = ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( - 𝑦 · 𝑋 ) ) ) )
33 1 3 12 grpasscan1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( - 𝑦 · 𝑋 ) ∈ 𝐵 ) → ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( - 𝑦 · 𝑋 ) ) ) = ( - 𝑦 · 𝑋 ) )
34 5 7 11 33 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + ( - 𝑦 · 𝑋 ) ) ) = ( - 𝑦 · 𝑋 ) )
35 17 32 34 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( 𝑋 + ( - 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( - 𝑦 · 𝑋 ) )
36 35 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( ( 𝑋 + ( - 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = ( ( - 𝑦 · 𝑋 ) + 𝑋 ) )
37 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( - 𝑦 · 𝑋 ) ∈ 𝐵 ) → ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ∈ 𝐵 )
38 4 6 10 37 syl3anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ∈ 𝐵 )
39 38 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ∈ 𝐵 )
40 1 3 12 grpasscan2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑋 + ( - 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) )
41 5 39 7 40 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( ( 𝑋 + ( - 𝑦 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) )
42 36 41 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) )