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	$$⊢\phi \to K\in V$$
	sgrppropd.l	$$⊢\phi \to L\in W$$
	sgrppropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	sgrppropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	sgrppropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
Assertion	sgrppropd	Could not format assertion : No typesetting found for |- ( ph -> ( K e. Smgrp <-> L e. Smgrp ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sgrppropd.k	$$⊢\phi \to K\in V$$
2		sgrppropd.l	$$⊢\phi \to L\in W$$
3		sgrppropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
4		sgrppropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
5		sgrppropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
6		simplr	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> K e. Smgrp ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> K e. Smgrp ) with typecode |-
7		simprl	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. B ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. B ) with typecode |-
8	3	ad2antrr	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> B = ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> B = ( Base ` K ) ) with typecode |-
9	7 8	eleqtrd	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` K ) ) with typecode |-
10		simprr	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. B ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. B ) with typecode |-
11	10 8	eleqtrd	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` K ) ) with typecode |-
12		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
13		eqid	$$⊢{+}_K={+}_K$$
14	12 13	sgrpcl	Could not format ( ( K e. Smgrp /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x ( +g ` K ) y ) e. ( Base ` K ) ) : No typesetting found for |- ( ( K e. Smgrp /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x ( +g ` K ) y ) e. ( Base ` K ) ) with typecode |-
15	6 9 11 14	syl3anc	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. ( Base ` K ) ) with typecode |-
16	15 8	eleqtrrd	Could not format ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. B ) : No typesetting found for |- ( ( ( ph /\ K e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. B ) with typecode |-
17	16	ralrimivva	Could not format ( ( ph /\ K e. Smgrp ) -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) : No typesetting found for |- ( ( ph /\ K e. Smgrp ) -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) with typecode |-
18	17	ex	Could not format ( ph -> ( K e. Smgrp -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) ) : No typesetting found for |- ( ph -> ( K e. Smgrp -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) ) with typecode |-
19		simplr	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> L e. Smgrp ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> L e. Smgrp ) with typecode |-
20		simprl	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. B ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. B ) with typecode |-
21	4	ad2antrr	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> B = ( Base ` L ) ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> B = ( Base ` L ) ) with typecode |-
22	20 21	eleqtrd	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` L ) ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` L ) ) with typecode |-
23		simprr	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. B ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. B ) with typecode |-
24	23 21	eleqtrd	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` L ) ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` L ) ) with typecode |-
25		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
26		eqid	$$⊢{+}_L={+}_L$$
27	25 26	sgrpcl	Could not format ( ( L e. Smgrp /\ x e. ( Base ` L ) /\ y e. ( Base ` L ) ) -> ( x ( +g ` L ) y ) e. ( Base ` L ) ) : No typesetting found for |- ( ( L e. Smgrp /\ x e. ( Base ` L ) /\ y e. ( Base ` L ) ) -> ( x ( +g ` L ) y ) e. ( Base ` L ) ) with typecode |-
28	19 22 24 27	syl3anc	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` L ) y ) e. ( Base ` L ) ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` L ) y ) e. ( Base ` L ) ) with typecode |-
29	5	adantlr	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) ) with typecode |-
30	28 29 21	3eltr4d	Could not format ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. B ) : No typesetting found for |- ( ( ( ph /\ L e. Smgrp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. B ) with typecode |-
31	30	ralrimivva	Could not format ( ( ph /\ L e. Smgrp ) -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) : No typesetting found for |- ( ( ph /\ L e. Smgrp ) -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) with typecode |-
32	31	ex	Could not format ( ph -> ( L e. Smgrp -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) ) : No typesetting found for |- ( ph -> ( L e. Smgrp -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) ) with typecode |-
33	12 13	issgrpv	Could not format ( K e. V -> ( K e. Smgrp <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) ) : No typesetting found for |- ( K e. V -> ( K e. Smgrp <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) ) with typecode |-
34	1 33	syl	Could not format ( ph -> ( K e. Smgrp <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) ) : No typesetting found for |- ( ph -> ( K e. Smgrp <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) ) with typecode |-
35	34	adantr	Could not format ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( K e. Smgrp <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( K e. Smgrp <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) ) with typecode |-
36	5	oveqrspc2v	$$⊢\left(\phi \wedge \left(u\in B\wedge v\in B\right)\right)\to u{+}_{K}v=u{+}_{L}v$$
37	36	adantlr	$$⊢\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\to u{+}_{K}v=u{+}_{L}v$$
38	37	eleq1d	$$⊢\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\to \left(u{+}_{K}v\in B\leftrightarrow u{+}_{L}v\in B\right)$$
39		simplll	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to \phi$$
40		simplrl	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to u\in B$$
41		simplrr	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to v\in B$$
42		simpllr	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to \forall x\in B\forall y\in Bx{+}_{K}y\in B$$
43		ovrspc2v	$$⊢\left(\left(u\in B\wedge v\in B\right)\wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to u{+}_{K}v\in B$$
44	40 41 42 43	syl21anc	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to u{+}_{K}v\in B$$
45		simpr	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to w\in B$$
46	5	oveqrspc2v	$$⊢\left(\phi \wedge \left(u{+}_{K}v\in B\wedge w\in B\right)\right)\to \left(u{+}_{K}v\right){+}_{K}w=\left(u{+}_{K}v\right){+}_{L}w$$
47	39 44 45 46	syl12anc	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to \left(u{+}_{K}v\right){+}_{K}w=\left(u{+}_{K}v\right){+}_{L}w$$
48	39 40 41 36	syl12anc	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to u{+}_{K}v=u{+}_{L}v$$
49	48	oveq1d	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to \left(u{+}_{K}v\right){+}_{L}w=\left(u{+}_{L}v\right){+}_{L}w$$
50	47 49	eqtrd	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to \left(u{+}_{K}v\right){+}_{K}w=\left(u{+}_{L}v\right){+}_{L}w$$
51		ovrspc2v	$$⊢\left(\left(v\in B\wedge w\in B\right)\wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to v{+}_{K}w\in B$$
52	41 45 42 51	syl21anc	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to v{+}_{K}w\in B$$
53	5	oveqrspc2v	$$⊢\left(\phi \wedge \left(u\in B\wedge v{+}_{K}w\in B\right)\right)\to u{+}_K\left(v{+}_{K}w\right)=u{+}_L\left(v{+}_{K}w\right)$$
54	39 40 52 53	syl12anc	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to u{+}_K\left(v{+}_{K}w\right)=u{+}_L\left(v{+}_{K}w\right)$$
55	5	oveqrspc2v	$$⊢\left(\phi \wedge \left(v\in B\wedge w\in B\right)\right)\to v{+}_{K}w=v{+}_{L}w$$
56	39 41 45 55	syl12anc	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to v{+}_{K}w=v{+}_{L}w$$
57	56	oveq2d	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to u{+}_L\left(v{+}_{K}w\right)=u{+}_L\left(v{+}_{L}w\right)$$
58	54 57	eqtrd	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to u{+}_K\left(v{+}_{K}w\right)=u{+}_L\left(v{+}_{L}w\right)$$
59	50 58	eqeq12d	$$⊢\left(\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\wedge w\in B\right)\to \left(\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\leftrightarrow \left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)$$
60	59	ralbidva	$$⊢\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\to \left(\forall w\in B\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\leftrightarrow \forall w\in B\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)$$
61	38 60	anbi12d	$$⊢\left(\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\wedge \left(u\in B\wedge v\in B\right)\right)\to \left(\left(u{+}_{K}v\in B\wedge \forall w\in B\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\leftrightarrow \left(u{+}_{L}v\in B\wedge \forall w\in B\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\right)$$
62	61	2ralbidva	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall u\in B\forall v\in B\left(u{+}_{K}v\in B\wedge \forall w\in B\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\leftrightarrow \forall u\in B\forall v\in B\left(u{+}_{L}v\in B\wedge \forall w\in B\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\right)$$
63	3	adantr	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to B={\mathrm{Base}}_K$$
64	63	eleq2d	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(u{+}_{K}v\in B\leftrightarrow u{+}_{K}v\in {\mathrm{Base}}_K\right)$$
65	63	raleqdv	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall w\in B\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\leftrightarrow \forall w\in {\mathrm{Base}}_K\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)$$
66	64 65	anbi12d	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\left(u{+}_{K}v\in B\wedge \forall w\in B\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\leftrightarrow \left(u{+}_{K}v\in {\mathrm{Base}}_K\wedge \forall w\in {\mathrm{Base}}_K\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\right)$$
67	63 66	raleqbidv	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall v\in B\left(u{+}_{K}v\in B\wedge \forall w\in B\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\leftrightarrow \forall v\in {\mathrm{Base}}_K\left(u{+}_{K}v\in {\mathrm{Base}}_K\wedge \forall w\in {\mathrm{Base}}_K\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\right)$$
68	63 67	raleqbidv	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall u\in B\forall v\in B\left(u{+}_{K}v\in B\wedge \forall w\in B\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\leftrightarrow \forall u\in {\mathrm{Base}}_K\forall v\in {\mathrm{Base}}_K\left(u{+}_{K}v\in {\mathrm{Base}}_K\wedge \forall w\in {\mathrm{Base}}_K\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\right)$$
69	4	adantr	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to B={\mathrm{Base}}_L$$
70	69	eleq2d	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(u{+}_{L}v\in B\leftrightarrow u{+}_{L}v\in {\mathrm{Base}}_L\right)$$
71	69	raleqdv	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall w\in B\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\leftrightarrow \forall w\in {\mathrm{Base}}_L\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)$$
72	70 71	anbi12d	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\left(u{+}_{L}v\in B\wedge \forall w\in B\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\leftrightarrow \left(u{+}_{L}v\in {\mathrm{Base}}_L\wedge \forall w\in {\mathrm{Base}}_L\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\right)$$
73	69 72	raleqbidv	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall v\in B\left(u{+}_{L}v\in B\wedge \forall w\in B\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\leftrightarrow \forall v\in {\mathrm{Base}}_L\left(u{+}_{L}v\in {\mathrm{Base}}_L\wedge \forall w\in {\mathrm{Base}}_L\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\right)$$
74	69 73	raleqbidv	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall u\in B\forall v\in B\left(u{+}_{L}v\in B\wedge \forall w\in B\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\leftrightarrow \forall u\in {\mathrm{Base}}_L\forall v\in {\mathrm{Base}}_L\left(u{+}_{L}v\in {\mathrm{Base}}_L\wedge \forall w\in {\mathrm{Base}}_L\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\right)$$
75	62 68 74	3bitr3d	$$⊢\left(\phi \wedge \forall x\in B\forall y\in Bx{+}_{K}y\in B\right)\to \left(\forall u\in {\mathrm{Base}}_K\forall v\in {\mathrm{Base}}_K\left(u{+}_{K}v\in {\mathrm{Base}}_K\wedge \forall w\in {\mathrm{Base}}_K\left(u{+}_{K}v\right){+}_{K}w=u{+}_K\left(v{+}_{K}w\right)\right)\leftrightarrow \forall u\in {\mathrm{Base}}_L\forall v\in {\mathrm{Base}}_L\left(u{+}_{L}v\in {\mathrm{Base}}_L\wedge \forall w\in {\mathrm{Base}}_L\left(u{+}_{L}v\right){+}_{L}w=u{+}_L\left(v{+}_{L}w\right)\right)\right)$$
76	25 26	issgrpv	Could not format ( L e. W -> ( L e. Smgrp <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) ) : No typesetting found for |- ( L e. W -> ( L e. Smgrp <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) ) with typecode |-
77	2 76	syl	Could not format ( ph -> ( L e. Smgrp <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) ) : No typesetting found for |- ( ph -> ( L e. Smgrp <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) ) with typecode |-
78	77	bicomd	Could not format ( ph -> ( A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) <-> L e. Smgrp ) ) : No typesetting found for |- ( ph -> ( A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) <-> L e. Smgrp ) ) with typecode |-
79	78	adantr	Could not format ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) <-> L e. Smgrp ) ) : No typesetting found for |- ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) <-> L e. Smgrp ) ) with typecode |-
80	35 75 79	3bitrd	Could not format ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( K e. Smgrp <-> L e. Smgrp ) ) : No typesetting found for |- ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( K e. Smgrp <-> L e. Smgrp ) ) with typecode |-
81	80	ex	Could not format ( ph -> ( A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B -> ( K e. Smgrp <-> L e. Smgrp ) ) ) : No typesetting found for |- ( ph -> ( A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B -> ( K e. Smgrp <-> L e. Smgrp ) ) ) with typecode |-
82	18 32 81	pm5.21ndd	Could not format ( ph -> ( K e. Smgrp <-> L e. Smgrp ) ) : No typesetting found for |- ( ph -> ( K e. Smgrp <-> L e. Smgrp ) ) with typecode |-