MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sgrppropd Structured version   Visualization version   GIF version

Theorem sgrppropd 18657
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.)
Hypotheses
Ref Expression
sgrppropd.k (𝜑𝐾𝑉)
sgrppropd.l (𝜑𝐿𝑊)
sgrppropd.1 (𝜑𝐵 = (Base‘𝐾))
sgrppropd.2 (𝜑𝐵 = (Base‘𝐿))
sgrppropd.3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
Assertion
Ref Expression
sgrppropd (𝜑 → (𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦   𝜑,𝑥,𝑦   𝑥,𝐿,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem sgrppropd
Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 766 . . . . . 6 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝐾 ∈ Smgrp)
2 simprl 768 . . . . . . 7 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
3 sgrppropd.1 . . . . . . . 8 (𝜑𝐵 = (Base‘𝐾))
43ad2antrr 723 . . . . . . 7 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝐵 = (Base‘𝐾))
52, 4eleqtrd 2834 . . . . . 6 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 ∈ (Base‘𝐾))
6 simprr 770 . . . . . . 7 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
76, 4eleqtrd 2834 . . . . . 6 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 ∈ (Base‘𝐾))
8 eqid 2731 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
9 eqid 2731 . . . . . . 7 (+g𝐾) = (+g𝐾)
108, 9sgrpcl 18652 . . . . . 6 ((𝐾 ∈ Smgrp ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑥(+g𝐾)𝑦) ∈ (Base‘𝐾))
111, 5, 7, 10syl3anc 1370 . . . . 5 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) ∈ (Base‘𝐾))
1211, 4eleqtrrd 2835 . . . 4 (((𝜑𝐾 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) ∈ 𝐵)
1312ralrimivva 3199 . . 3 ((𝜑𝐾 ∈ Smgrp) → ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵)
1413ex 412 . 2 (𝜑 → (𝐾 ∈ Smgrp → ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵))
15 simplr 766 . . . . . 6 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝐿 ∈ Smgrp)
16 simprl 768 . . . . . . 7 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
17 sgrppropd.2 . . . . . . . 8 (𝜑𝐵 = (Base‘𝐿))
1817ad2antrr 723 . . . . . . 7 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝐵 = (Base‘𝐿))
1916, 18eleqtrd 2834 . . . . . 6 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 ∈ (Base‘𝐿))
20 simprr 770 . . . . . . 7 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
2120, 18eleqtrd 2834 . . . . . 6 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 ∈ (Base‘𝐿))
22 eqid 2731 . . . . . . 7 (Base‘𝐿) = (Base‘𝐿)
23 eqid 2731 . . . . . . 7 (+g𝐿) = (+g𝐿)
2422, 23sgrpcl 18652 . . . . . 6 ((𝐿 ∈ Smgrp ∧ 𝑥 ∈ (Base‘𝐿) ∧ 𝑦 ∈ (Base‘𝐿)) → (𝑥(+g𝐿)𝑦) ∈ (Base‘𝐿))
2515, 19, 21, 24syl3anc 1370 . . . . 5 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐿)𝑦) ∈ (Base‘𝐿))
26 sgrppropd.3 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
2726adantlr 712 . . . . 5 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
2825, 27, 183eltr4d 2847 . . . 4 (((𝜑𝐿 ∈ Smgrp) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) ∈ 𝐵)
2928ralrimivva 3199 . . 3 ((𝜑𝐿 ∈ Smgrp) → ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵)
3029ex 412 . 2 (𝜑 → (𝐿 ∈ Smgrp → ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵))
31 sgrppropd.k . . . . . 6 (𝜑𝐾𝑉)
328, 9issgrpv 18647 . . . . . 6 (𝐾𝑉 → (𝐾 ∈ Smgrp ↔ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾) ∧ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)))))
3331, 32syl 17 . . . . 5 (𝜑 → (𝐾 ∈ Smgrp ↔ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾) ∧ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)))))
3433adantr 480 . . . 4 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (𝐾 ∈ Smgrp ↔ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾) ∧ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)))))
3526oveqrspc2v 7439 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝐵𝑣𝐵)) → (𝑢(+g𝐾)𝑣) = (𝑢(+g𝐿)𝑣))
3635adantlr 712 . . . . . . . 8 (((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) → (𝑢(+g𝐾)𝑣) = (𝑢(+g𝐿)𝑣))
3736eleq1d 2817 . . . . . . 7 (((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) → ((𝑢(+g𝐾)𝑣) ∈ 𝐵 ↔ (𝑢(+g𝐿)𝑣) ∈ 𝐵))
38 simplll 772 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → 𝜑)
39 simplrl 774 . . . . . . . . . . . 12 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → 𝑢𝐵)
40 simplrr 775 . . . . . . . . . . . 12 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → 𝑣𝐵)
41 simpllr 773 . . . . . . . . . . . 12 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵)
42 ovrspc2v 7438 . . . . . . . . . . . 12 (((𝑢𝐵𝑣𝐵) ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (𝑢(+g𝐾)𝑣) ∈ 𝐵)
4339, 40, 41, 42syl21anc 835 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (𝑢(+g𝐾)𝑣) ∈ 𝐵)
44 simpr 484 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → 𝑤𝐵)
4526oveqrspc2v 7439 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑢(+g𝐾)𝑣) ∈ 𝐵𝑤𝐵)) → ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = ((𝑢(+g𝐾)𝑣)(+g𝐿)𝑤))
4638, 43, 44, 45syl12anc 834 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = ((𝑢(+g𝐾)𝑣)(+g𝐿)𝑤))
4738, 39, 40, 35syl12anc 834 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (𝑢(+g𝐾)𝑣) = (𝑢(+g𝐿)𝑣))
4847oveq1d 7427 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → ((𝑢(+g𝐾)𝑣)(+g𝐿)𝑤) = ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤))
4946, 48eqtrd 2771 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤))
50 ovrspc2v 7438 . . . . . . . . . . . 12 (((𝑣𝐵𝑤𝐵) ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (𝑣(+g𝐾)𝑤) ∈ 𝐵)
5140, 44, 41, 50syl21anc 835 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (𝑣(+g𝐾)𝑤) ∈ 𝐵)
5226oveqrspc2v 7439 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝐵 ∧ (𝑣(+g𝐾)𝑤) ∈ 𝐵)) → (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)) = (𝑢(+g𝐿)(𝑣(+g𝐾)𝑤)))
5338, 39, 51, 52syl12anc 834 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)) = (𝑢(+g𝐿)(𝑣(+g𝐾)𝑤)))
5426oveqrspc2v 7439 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝐵𝑤𝐵)) → (𝑣(+g𝐾)𝑤) = (𝑣(+g𝐿)𝑤))
5538, 40, 44, 54syl12anc 834 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (𝑣(+g𝐾)𝑤) = (𝑣(+g𝐿)𝑤))
5655oveq2d 7428 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (𝑢(+g𝐿)(𝑣(+g𝐾)𝑤)) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))
5753, 56eqtrd 2771 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))
5849, 57eqeq12d 2747 . . . . . . . 8 ((((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) ∧ 𝑤𝐵) → (((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)) ↔ ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))))
5958ralbidva 3174 . . . . . . 7 (((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) → (∀𝑤𝐵 ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)) ↔ ∀𝑤𝐵 ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))))
6037, 59anbi12d 630 . . . . . 6 (((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) ∧ (𝑢𝐵𝑣𝐵)) → (((𝑢(+g𝐾)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤))) ↔ ((𝑢(+g𝐿)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
61602ralbidva 3215 . . . . 5 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑢𝐵𝑣𝐵 ((𝑢(+g𝐾)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤))) ↔ ∀𝑢𝐵𝑣𝐵 ((𝑢(+g𝐿)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
623adantr 480 . . . . . 6 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → 𝐵 = (Base‘𝐾))
6362eleq2d 2818 . . . . . . . 8 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → ((𝑢(+g𝐾)𝑣) ∈ 𝐵 ↔ (𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾)))
6462raleqdv 3324 . . . . . . . 8 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑤𝐵 ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)) ↔ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤))))
6563, 64anbi12d 630 . . . . . . 7 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (((𝑢(+g𝐾)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤))) ↔ ((𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾) ∧ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)))))
6662, 65raleqbidv 3341 . . . . . 6 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑣𝐵 ((𝑢(+g𝐾)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤))) ↔ ∀𝑣 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾) ∧ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)))))
6762, 66raleqbidv 3341 . . . . 5 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑢𝐵𝑣𝐵 ((𝑢(+g𝐾)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤))) ↔ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾) ∧ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤)))))
6817adantr 480 . . . . . 6 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → 𝐵 = (Base‘𝐿))
6968eleq2d 2818 . . . . . . . 8 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → ((𝑢(+g𝐿)𝑣) ∈ 𝐵 ↔ (𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿)))
7068raleqdv 3324 . . . . . . . 8 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑤𝐵 ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)) ↔ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))))
7169, 70anbi12d 630 . . . . . . 7 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (((𝑢(+g𝐿)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))) ↔ ((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
7268, 71raleqbidv 3341 . . . . . 6 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑣𝐵 ((𝑢(+g𝐿)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))) ↔ ∀𝑣 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
7368, 72raleqbidv 3341 . . . . 5 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑢𝐵𝑣𝐵 ((𝑢(+g𝐿)𝑣) ∈ 𝐵 ∧ ∀𝑤𝐵 ((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))) ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
7461, 67, 733bitr3d 309 . . . 4 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣) ∈ (Base‘𝐾) ∧ ∀𝑤 ∈ (Base‘𝐾)((𝑢(+g𝐾)𝑣)(+g𝐾)𝑤) = (𝑢(+g𝐾)(𝑣(+g𝐾)𝑤))) ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
75 sgrppropd.l . . . . . . 7 (𝜑𝐿𝑊)
7622, 23issgrpv 18647 . . . . . . 7 (𝐿𝑊 → (𝐿 ∈ Smgrp ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
7775, 76syl 17 . . . . . 6 (𝜑 → (𝐿 ∈ Smgrp ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤)))))
7877bicomd 222 . . . . 5 (𝜑 → (∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))) ↔ 𝐿 ∈ Smgrp))
7978adantr 480 . . . 4 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣) ∈ (Base‘𝐿) ∧ ∀𝑤 ∈ (Base‘𝐿)((𝑢(+g𝐿)𝑣)(+g𝐿)𝑤) = (𝑢(+g𝐿)(𝑣(+g𝐿)𝑤))) ↔ 𝐿 ∈ Smgrp))
8034, 74, 793bitrd 305 . . 3 ((𝜑 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵) → (𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp))
8180ex 412 . 2 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) ∈ 𝐵 → (𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp)))
8214, 30, 81pm5.21ndd 379 1 (𝜑 → (𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1540  wcel 2105  wral 3060  cfv 6543  (class class class)co 7412  Basecbs 17149  +gcplusg 17202  Smgrpcsgrp 18644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-mgm 18566  df-sgrp 18645
This theorem is referenced by:  rngpropd  20069  prdsrngd  20071
  Copyright terms: Public domain W3C validator