Theorem sgrppropd

Description: If two structures are sets, have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a semigroup iff the other one is. (Contributed by AV, 15-Feb-2025)

	Ref	Expression
Hypotheses	sgrppropd.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	sgrppropd.l	⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
	sgrppropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	sgrppropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	sgrppropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
Assertion	sgrppropd	⊢ ( 𝜑 → ( 𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp ) )

Proof

Step	Hyp	Ref	Expression
1		sgrppropd.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
2		sgrppropd.l	⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
3		sgrppropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
4		sgrppropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
5		sgrppropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
6		simplr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐾 ∈ Smgrp )
7		simprl	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
8	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
9	7 8	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
10		simprr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
11	10 8	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
12		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13		eqid	⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
14	12 13	sgrpcl	⊢ ( ( 𝐾 ∈ Smgrp ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
15	6 9 11 14	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
16	15 8	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
17	16	ralrimivva	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Smgrp ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
18	17	ex	⊢ ( 𝜑 → ( 𝐾 ∈ Smgrp → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
19		simplr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐿 ∈ Smgrp )
20		simprl	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
21	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
22	20 21	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐿 ) )
23		simprr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
24	23 21	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐿 ) )
25		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
26		eqid	⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
27	25 26	sgrpcl	⊢ ( ( 𝐿 ∈ Smgrp ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
28	19 22 24 27	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
29	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
30	28 29 21	3eltr4d	⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
31	30	ralrimivva	⊢ ( ( 𝜑 ∧ 𝐿 ∈ Smgrp ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
32	31	ex	⊢ ( 𝜑 → ( 𝐿 ∈ Smgrp → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
33	12 13	issgrpv	⊢ ( 𝐾 ∈ 𝑉 → ( 𝐾 ∈ Smgrp ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
34	1 33	syl	⊢ ( 𝜑 → ( 𝐾 ∈ Smgrp ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝐾 ∈ Smgrp ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
36	5	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) )
37	36	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) )
38	37	eleq1d	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ↔ ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ) )
39		simplll	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝜑 )
40		simplrl	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
41		simplrr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
42		simpllr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
43		ovrspc2v	⊢ ( ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 )
44	40 41 42 43	syl21anc	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 )
45		simpr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝐵 )
46	5	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
47	39 44 45 46	syl12anc	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
48	39 40 41 36	syl12anc	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) )
49	48	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
50	47 49	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
51		ovrspc2v	⊢ ( ( ( 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
52	41 45 42 51	syl21anc	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
53	5	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) )
54	39 40 52 53	syl12anc	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) )
55	5	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) )
56	39 41 45 55	syl12anc	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) )
57	56	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) )
58	54 57	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) )
59	50 58	eqeq12d	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) )
60	59	ralbidva	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) )
61	38 60	anbi12d	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
62	61	2ralbidva	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
63	3	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐾 ) )
64	63	eleq2d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ↔ ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ) )
65	63	raleqdv	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) )
66	64 65	anbi12d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
67	63 66	raleqbidv	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
68	63 67	raleqbidv	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
69	4	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐿 ) )
70	69	eleq2d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ↔ ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ) )
71	69	raleqdv	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) )
72	70 71	anbi12d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
73	69 72	raleqbidv	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
74	69 73	raleqbidv	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
75	62 68 74	3bitr3d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
76	25 26	issgrpv	⊢ ( 𝐿 ∈ 𝑊 → ( 𝐿 ∈ Smgrp ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
77	2 76	syl	⊢ ( 𝜑 → ( 𝐿 ∈ Smgrp ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
78	77	bicomd	⊢ ( 𝜑 → ( ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ 𝐿 ∈ Smgrp ) )
79	78	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ 𝐿 ∈ Smgrp ) )
80	35 75 79	3bitrd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp ) )
81	80	ex	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 → ( 𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp ) ) )
82	18 32 81	pm5.21ndd	⊢ ( 𝜑 → ( 𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp ) )