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	⊢ ( 𝜑 → · = × )