This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )