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 ⊢ × = ( .g ‘ 𝐻 )
mulgpropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
mulgpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐻 ) )
mulgpropd.i ⊢ ( 𝜑 → 𝐵 ⊆ 𝐾 )
mulgpropd.k ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐾 )
mulgpropd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
Assertion mulgpropd ( 𝜑 → · = × )

Proof

Step Hyp Ref Expression
1 mulgpropd.m ⊢ · = ( .g ‘ 𝐺 )
2 mulgpropd.n ⊢ × = ( .g ‘ 𝐻 )
3 mulgpropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
4 mulgpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐻 ) )
5 mulgpropd.i ⊢ ( 𝜑 → 𝐵 ⊆ 𝐾 )
6 mulgpropd.k ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐾 )
7 mulgpropd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
8 ssel ⊢ ( 𝐵 ⊆ 𝐾 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐾 ) )
9 ssel ⊢ ( 𝐵 ⊆ 𝐾 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐾 ) )
10 8 9 anim12d ⊢ ( 𝐵 ⊆ 𝐾 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) )
11 5 10 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) )
12 11 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) )
13 12 7 syldan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
14 3 4 13 grpidpropd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
15 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
16 1zzd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ ℤ )
17 vex ⊢ 𝑏 ∈ V
18 17 fvconst2 ⊢ ( 𝑥 ∈ ℕ → ( ( ℕ × { 𝑏 } ) ‘ 𝑥 ) = 𝑏 )
19 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
20 19 eqcomi ⊢ ( ℤ≥ ‘ 1 ) = ℕ
21 18 20 eleq2s ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) → ( ( ℕ × { 𝑏 } ) ‘ 𝑥 ) = 𝑏 )
22 21 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( ℕ × { 𝑏 } ) ‘ 𝑥 ) = 𝑏 )
23 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ⊆ 𝐾 )
24 simp3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
25 23 24 sseldd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐾 )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑏 ∈ 𝐾 )
27 22 26 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( ℕ × { 𝑏 } ) ‘ 𝑥 ) ∈ 𝐾 )
28 6 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐾 )
29 7 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
30 16 27 28 29 seqfeq3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) )
31 30 fveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) )
32 3 4 13 grpinvpropd ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) = ( invg ‘ 𝐻 ) )
33 32 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → ( invg ‘ 𝐺 ) = ( invg ‘ 𝐻 ) )
34 30 fveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) )
35 33 34 fveq12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) )
36 31 35 ifeq12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) = if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) )
37 15 36 ifeq12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵 ) → if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) = if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) )
38 37 mpoeq3dva ⊢ ( 𝜑 → ( 𝑎 ∈ ℤ , 𝑏 ∈ 𝐵 ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) = ( 𝑎 ∈ ℤ , 𝑏 ∈ 𝐵 ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) )
39 eqidd ⊢ ( 𝜑 → ℤ = ℤ )
40 eqidd ⊢ ( 𝜑 → if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) = if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) )
41 39 3 40 mpoeq123dv ⊢ ( 𝜑 → ( 𝑎 ∈ ℤ , 𝑏 ∈ 𝐵 ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) = ( 𝑎 ∈ ℤ , 𝑏 ∈ ( Base ‘ 𝐺 ) ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) )
42 eqidd ⊢ ( 𝜑 → if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) = if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) )
43 39 4 42 mpoeq123dv ⊢ ( 𝜑 → ( 𝑎 ∈ ℤ , 𝑏 ∈ 𝐵 ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) = ( 𝑎 ∈ ℤ , 𝑏 ∈ ( Base ‘ 𝐻 ) ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) )
44 38 41 43 3eqtr3d ⊢ ( 𝜑 → ( 𝑎 ∈ ℤ , 𝑏 ∈ ( Base ‘ 𝐺 ) ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) = ( 𝑎 ∈ ℤ , 𝑏 ∈ ( Base ‘ 𝐻 ) ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) ) )
45 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
46 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
47 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
48 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
49 45 46 47 48 1 mulgfval ⊢ · = ( 𝑎 ∈ ℤ , 𝑏 ∈ ( Base ‘ 𝐺 ) ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) )
50 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
51 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
52 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
53 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
54 50 51 52 53 2 mulgfval ⊢ × = ( 𝑎 ∈ ℤ , 𝑏 ∈ ( Base ‘ 𝐻 ) ↦ if ( 𝑎 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑎 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ 𝑎 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑏 } ) ) ‘ - 𝑎 ) ) ) ) )
55 44 49 54 3eqtr4g ⊢ ( 𝜑 → · = × )