Metamath Proof Explorer

Theorem mulgpropd

Description: Two structures with the same group-nature have the same group multiple function. K is expected to either be _V (when strong equality is available) or B (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mulgpropd.m ⊢·˙=⋅G
mulgpropd.n ⊢×˙=⋅H
mulgpropd.b1 ⊢φ→B=BaseG
mulgpropd.b2 ⊢φ→B=BaseH
mulgpropd.i ⊢φ→B⊆K
mulgpropd.k ⊢φ∧x∈K∧y∈K→x+Gy∈K
mulgpropd.e ⊢φ∧x∈K∧y∈K→x+Gy=x+Hy
Assertion mulgpropd ⊢φ→·˙=×˙

Proof

Step Hyp Ref Expression
1 mulgpropd.m ⊢·˙=⋅G
2 mulgpropd.n ⊢×˙=⋅H
3 mulgpropd.b1 ⊢φ→B=BaseG
4 mulgpropd.b2 ⊢φ→B=BaseH
5 mulgpropd.i ⊢φ→B⊆K
6 mulgpropd.k ⊢φ∧x∈K∧y∈K→x+Gy∈K
7 mulgpropd.e ⊢φ∧x∈K∧y∈K→x+Gy=x+Hy
8 ssel ⊢B⊆K→x∈B→x∈K
9 ssel ⊢B⊆K→y∈B→y∈K
10 8 9 anim12d ⊢B⊆K→x∈B∧y∈B→x∈K∧y∈K
11 5 10 syl ⊢φ→x∈B∧y∈B→x∈K∧y∈K
12 11 imp ⊢φ∧x∈B∧y∈B→x∈K∧y∈K
13 12 7 syldan ⊢φ∧x∈B∧y∈B→x+Gy=x+Hy
14 3 4 13 grpidpropd ⊢φ→0G=0H
15 14 3ad2ant1 ⊢φ∧a∈ℤ∧b∈B→0G=0H
16 1zzd ⊢φ∧a∈ℤ∧b∈B→1∈ℤ
17 vex ⊢b∈V
18 17 fvconst2 ⊢x∈ℕ→ℕ×b⁡x=b
19 nnuz ⊢ℕ=ℤ≥1
20 19 eqcomi ⊢ℤ≥1=ℕ
21 18 20 eleq2s ⊢x∈ℤ≥1→ℕ×b⁡x=b
22 21 adantl ⊢φ∧a∈ℤ∧b∈B∧x∈ℤ≥1→ℕ×b⁡x=b
23 5 3ad2ant1 ⊢φ∧a∈ℤ∧b∈B→B⊆K
24 simp3 ⊢φ∧a∈ℤ∧b∈B→b∈B
25 23 24 sseldd ⊢φ∧a∈ℤ∧b∈B→b∈K
26 25 adantr ⊢φ∧a∈ℤ∧b∈B∧x∈ℤ≥1→b∈K
27 22 26 eqeltrd ⊢φ∧a∈ℤ∧b∈B∧x∈ℤ≥1→ℕ×b⁡x∈K
28 6 3ad2antl1 ⊢φ∧a∈ℤ∧b∈B∧x∈K∧y∈K→x+Gy∈K
29 7 3ad2antl1 ⊢φ∧a∈ℤ∧b∈B∧x∈K∧y∈K→x+Gy=x+Hy
30 16 27 28 29 seqfeq3 ⊢φ∧a∈ℤ∧b∈B→seq1+Gℕ×b=seq1+Hℕ×b
31 30 fveq1d ⊢φ∧a∈ℤ∧b∈B→seq1+Gℕ×b⁡a=seq1+Hℕ×b⁡a
32 3 4 13 grpinvpropd ⊢φ→invg⁡G=invg⁡H
33 32 3ad2ant1 ⊢φ∧a∈ℤ∧b∈B→invg⁡G=invg⁡H
34 30 fveq1d ⊢φ∧a∈ℤ∧b∈B→seq1+Gℕ×b⁡−a=seq1+Hℕ×b⁡−a
35 33 34 fveq12d ⊢φ∧a∈ℤ∧b∈B→invg⁡G⁡seq1+Gℕ×b⁡−a=invg⁡H⁡seq1+Hℕ×b⁡−a
36 31 35 ifeq12d ⊢φ∧a∈ℤ∧b∈B→if0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a=if0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a
37 15 36 ifeq12d ⊢φ∧a∈ℤ∧b∈B→ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a=ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a
38 37 mpoeq3dva ⊢φ→a∈ℤ,b∈B⟼ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a=a∈ℤ,b∈B⟼ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a
39 eqidd ⊢φ→ℤ=ℤ
40 eqidd ⊢φ→ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a=ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a
41 39 3 40 mpoeq123dv ⊢φ→a∈ℤ,b∈B⟼ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a=a∈ℤ,b∈BaseG⟼ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a
42 eqidd ⊢φ→ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a=ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a
43 39 4 42 mpoeq123dv ⊢φ→a∈ℤ,b∈B⟼ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a=a∈ℤ,b∈BaseH⟼ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a
44 38 41 43 3eqtr3d ⊢φ→a∈ℤ,b∈BaseG⟼ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a=a∈ℤ,b∈BaseH⟼ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a
45 eqid ⊢BaseG=BaseG
46 eqid ⊢+G=+G
47 eqid ⊢0G=0G
48 eqid ⊢invg⁡G=invg⁡G
49 45 46 47 48 1 mulgfval ⊢·˙=a∈ℤ,b∈BaseG⟼ifa=00Gif0<aseq1+Gℕ×b⁡ainvg⁡G⁡seq1+Gℕ×b⁡−a
50 eqid ⊢BaseH=BaseH
51 eqid ⊢+H=+H
52 eqid ⊢0H=0H
53 eqid ⊢invg⁡H=invg⁡H
54 50 51 52 53 2 mulgfval ⊢×˙=a∈ℤ,b∈BaseH⟼ifa=00Hif0<aseq1+Hℕ×b⁡ainvg⁡H⁡seq1+Hℕ×b⁡−a
55 44 49 54 3eqtr4g ⊢φ→·˙=×˙