Theorem grppropd

Description: If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	grppropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	grppropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	grppropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
Assertion	grppropd	⊢ ( 𝜑 → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )

Proof

Step	Hyp	Ref	Expression
1		grppropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		grppropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		grppropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4	1 2 3	mndpropd	⊢ ( 𝜑 → ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd ) )
5	1 2 3	grpidpropd	⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
7	3 6	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
8	7	anass1rs	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
9	8	rexbidva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
10	9	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
11	1	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) )
12	1 11	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) )
13	2	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
14	2 13	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
15	10 12 14	3bitr3d	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
16	4 15	anbi12d	⊢ ( 𝜑 → ( ( 𝐾 ∈ Mnd ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) ↔ ( 𝐿 ∈ Mnd ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) ) )
17		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18		eqid	⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
19		eqid	⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
20	17 18 19	isgrp	⊢ ( 𝐾 ∈ Grp ↔ ( 𝐾 ∈ Mnd ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) )
21		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
22		eqid	⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
23		eqid	⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
24	21 22 23	isgrp	⊢ ( 𝐿 ∈ Grp ↔ ( 𝐿 ∈ Mnd ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
25	16 20 24	3bitr4g	⊢ ( 𝜑 → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )