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 = Base G
mulgpropd.b2 ⊢ φ → B = Base H
mulgpropd.i ⊢ φ → B ⊆ K
mulgpropd.k ⊢ φ ∧ x ∈ K ∧ y ∈ K → x + G y ∈ K
mulgpropd.e ⊢ φ ∧ x ∈ K ∧ y ∈ K → x + G y = x + H y
Assertion mulgpropd ⊢ φ → · ˙ = × ˙

Proof

Step Hyp Ref Expression
1 mulgpropd.m ⊢ · ˙ = ⋅ G
2 mulgpropd.n ⊢ × ˙ = ⋅ H
3 mulgpropd.b1 ⊢ φ → B = Base G
4 mulgpropd.b2 ⊢ φ → B = Base H
5 mulgpropd.i ⊢ φ → B ⊆ K
6 mulgpropd.k ⊢ φ ∧ x ∈ K ∧ y ∈ K → x + G y ∈ K
7 mulgpropd.e ⊢ φ ∧ x ∈ K ∧ y ∈ K → x + G y = x + H y
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 + G y = x + H y
14 3 4 13 grpidpropd ⊢ φ → 0 G = 0 H
15 14 3ad2ant1 ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → 0 G = 0 H
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 + G y ∈ K
29 7 3ad2antl1 ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B ∧ x ∈ K ∧ y ∈ K → x + G y = x + H y
30 16 27 28 29 seqfeq3 ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → seq 1 + G ℕ × b = seq 1 + H ℕ × b
31 30 fveq1d ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → seq 1 + G ℕ × b ⁡ a = seq 1 + H ℕ × b ⁡ a
32 3 4 13 grpinvpropd ⊢ φ → inv g ⁡ G = inv g ⁡ H
33 32 3ad2ant1 ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → inv g ⁡ G = inv g ⁡ H
34 30 fveq1d ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → seq 1 + G ℕ × b ⁡ − a = seq 1 + H ℕ × b ⁡ − a
35 33 34 fveq12d ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a = inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
36 31 35 ifeq12d ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a = if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
37 15 36 ifeq12d ⊢ φ ∧ a ∈ ℤ ∧ b ∈ B → if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a = if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
38 37 mpoeq3dva ⊢ φ → a ∈ ℤ , b ∈ B ⟼ if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a = a ∈ ℤ , b ∈ B ⟼ if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
39 eqidd ⊢ φ → ℤ = ℤ
40 eqidd ⊢ φ → if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a = if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a
41 39 3 40 mpoeq123dv ⊢ φ → a ∈ ℤ , b ∈ B ⟼ if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a = a ∈ ℤ , b ∈ Base G ⟼ if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a
42 eqidd ⊢ φ → if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a = if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
43 39 4 42 mpoeq123dv ⊢ φ → a ∈ ℤ , b ∈ B ⟼ if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a = a ∈ ℤ , b ∈ Base H ⟼ if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
44 38 41 43 3eqtr3d ⊢ φ → a ∈ ℤ , b ∈ Base G ⟼ if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a = a ∈ ℤ , b ∈ Base H ⟼ if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
45 eqid ⊢ Base G = Base G
46 eqid ⊢ + G = + G
47 eqid ⊢ 0 G = 0 G
48 eqid ⊢ inv g ⁡ G = inv g ⁡ G
49 45 46 47 48 1 mulgfval ⊢ · ˙ = a ∈ ℤ , b ∈ Base G ⟼ if a = 0 0 G if 0 < a seq 1 + G ℕ × b ⁡ a inv g ⁡ G ⁡ seq 1 + G ℕ × b ⁡ − a
50 eqid ⊢ Base H = Base H
51 eqid ⊢ + H = + H
52 eqid ⊢ 0 H = 0 H
53 eqid ⊢ inv g ⁡ H = inv g ⁡ H
54 50 51 52 53 2 mulgfval ⊢ × ˙ = a ∈ ℤ , b ∈ Base H ⟼ if a = 0 0 H if 0 < a seq 1 + H ℕ × b ⁡ a inv g ⁡ H ⁡ seq 1 + H ℕ × b ⁡ − a
55 44 49 54 3eqtr4g ⊢ φ → · ˙ = × ˙