Theorem rngpropd

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

	Ref	Expression
Hypotheses	rngpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	rngpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	rngpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	rngpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	rngpropd	$$⊢\phi \to \left(K\in \mathrm{Rng}\leftrightarrow L\in \mathrm{Rng}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rngpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		rngpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		rngpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4		rngpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
5		simpll	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ph ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ph ) with typecode |-
6		simprll	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. B ) with typecode |-
7		simplrl	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. Abel ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. Abel ) with typecode |-
8		simprlr	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. B ) with typecode |-
9	1	ad2antrr	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> B = ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> B = ( Base ` K ) ) with typecode |-
10	8 9	eleqtrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` K ) ) with typecode |-
11		simprr	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. B ) with typecode |-
12	11 9	eleqtrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` K ) ) with typecode |-
13		ablgrp	$$⊢K\in \mathrm{Abel}\to K\in \mathrm{Grp}$$
14		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
15		eqid	$$⊢{+}_K={+}_K$$
16	14 15	grpcl	$$⊢\left(K\in \mathrm{Grp}\wedge v\in {\mathrm{Base}}_K\wedge w\in {\mathrm{Base}}_K\right)\to v{+}_{K}w\in {\mathrm{Base}}_K$$
17	13 16	syl3an1	$$⊢\left(K\in \mathrm{Abel}\wedge v\in {\mathrm{Base}}_K\wedge w\in {\mathrm{Base}}_K\right)\to v{+}_{K}w\in {\mathrm{Base}}_K$$
18	7 10 12 17	syl3anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) ) with typecode |-
19	18 9	eleqtrrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. B ) with typecode |-
20	4	oveqrspc2v	$$⊢\left(\phi \wedge \left(u\in B\wedge v{+}_{K}w\in B\right)\right)\to u{\cdot }_K\left(v{+}_{K}w\right)=u{\cdot }_L\left(v{+}_{K}w\right)$$
21	5 6 19 20	syl12anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) ) with typecode |-
22	3	oveqrspc2v	$$⊢\left(\phi \wedge \left(v\in B\wedge w\in B\right)\right)\to v{+}_{K}w=v{+}_{L}w$$
23	5 8 11 22	syl12anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) ) with typecode |-
24	23	oveq2d	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` L ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` L ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) ) with typecode |-
25	21 24	eqtrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) ) with typecode |-
26		simplrr	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( mulGrp ` K ) e. Smgrp ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( mulGrp ` K ) e. Smgrp ) with typecode |-
27	6 9	eleqtrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` K ) ) with typecode |-
28		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
29	28 14	mgpbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
30		eqid	$$⊢{\cdot }_K={\cdot }_K$$
31	28 30	mgpplusg	$$⊢{\cdot }_K={+}_{{\mathrm{mulGrp}}_K}$$
32	29 31	sgrpcl	Could not format ( ( ( mulGrp ` K ) e. Smgrp /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( mulGrp ` K ) e. Smgrp /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) ) with typecode |-
33	26 27 10 32	syl3anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) ) with typecode |-
34	33 9	eleqtrrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. B ) with typecode |-
35	29 31	sgrpcl	Could not format ( ( ( mulGrp ` K ) e. Smgrp /\ u e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( mulGrp ` K ) e. Smgrp /\ u e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) ) with typecode |-
36	26 27 12 35	syl3anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) ) with typecode |-
37	36 9	eleqtrrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. B ) with typecode |-
38	3	oveqrspc2v	$$⊢\left(\phi \wedge \left(u{\cdot }_{K}v\in B\wedge u{\cdot }_{K}w\in B\right)\right)\to \left(u{\cdot }_{K}v\right){+}_K\left(u{\cdot }_{K}w\right)=\left(u{\cdot }_{K}v\right){+}_L\left(u{\cdot }_{K}w\right)$$
39	5 34 37 38	syl12anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) ) with typecode |-
40	4	oveqrspc2v	$$⊢\left(\phi \wedge \left(u\in B\wedge v\in B\right)\right)\to u{\cdot }_{K}v=u{\cdot }_{L}v$$
41	40	ad2ant2r	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) ) with typecode |-
42	4	oveqrspc2v	$$⊢\left(\phi \wedge \left(u\in B\wedge w\in B\right)\right)\to u{\cdot }_{K}w=u{\cdot }_{L}w$$
43	5 6 11 42	syl12anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) ) with typecode |-
44	41 43	oveq12d	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) with typecode |-
45	39 44	eqtrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) with typecode |-
46	25 45	eqeq12d	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) <-> ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) <-> ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) ) with typecode |-
47	14 15	grpcl	$$⊢\left(K\in \mathrm{Grp}\wedge u\in {\mathrm{Base}}_K\wedge v\in {\mathrm{Base}}_K\right)\to u{+}_{K}v\in {\mathrm{Base}}_K$$
48	13 47	syl3an1	$$⊢\left(K\in \mathrm{Abel}\wedge u\in {\mathrm{Base}}_K\wedge v\in {\mathrm{Base}}_K\right)\to u{+}_{K}v\in {\mathrm{Base}}_K$$
49	7 27 10 48	syl3anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) ) with typecode |-
50	49 9	eleqtrrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. B ) with typecode |-
51	4	oveqrspc2v	$$⊢\left(\phi \wedge \left(u{+}_{K}v\in B\wedge w\in B\right)\right)\to \left(u{+}_{K}v\right){\cdot }_{K}w=\left(u{+}_{K}v\right){\cdot }_{L}w$$
52	5 50 11 51	syl12anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) ) with typecode |-
53	3	oveqrspc2v	$$⊢\left(\phi \wedge \left(u\in B\wedge v\in B\right)\right)\to u{+}_{K}v=u{+}_{L}v$$
54	53	ad2ant2r	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) ) with typecode |-
55	54	oveq1d	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` L ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` L ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) ) with typecode |-
56	52 55	eqtrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) ) with typecode |-
57	29 31	sgrpcl	Could not format ( ( ( mulGrp ` K ) e. Smgrp /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( mulGrp ` K ) e. Smgrp /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) ) with typecode |-
58	26 10 12 57	syl3anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) ) with typecode |-
59	58 9	eleqtrrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. B ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. B ) with typecode |-
60	3	oveqrspc2v	$$⊢\left(\phi \wedge \left(u{\cdot }_{K}w\in B\wedge v{\cdot }_{K}w\in B\right)\right)\to \left(u{\cdot }_{K}w\right){+}_K\left(v{\cdot }_{K}w\right)=\left(u{\cdot }_{K}w\right){+}_L\left(v{\cdot }_{K}w\right)$$
61	5 37 59 60	syl12anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) ) with typecode |-
62	4	oveqrspc2v	$$⊢\left(\phi \wedge \left(v\in B\wedge w\in B\right)\right)\to v{\cdot }_{K}w=v{\cdot }_{L}w$$
63	5 8 11 62	syl12anc	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) ) with typecode |-
64	43 63	oveq12d	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) with typecode |-
65	61 64	eqtrd	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) with typecode |-
66	56 65	eqeq12d	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) <-> ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) <-> ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) with typecode |-
67	46 66	anbi12d	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
68	67	anassrs	Could not format ( ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
69	68	ralbidva	Could not format ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
70	69	2ralbidva	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
71	1	adantr	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` K ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` K ) ) with typecode |-
72	71	raleqdv	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) with typecode |-
73	71 72	raleqbidv	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) with typecode |-
74	71 73	raleqbidv	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) with typecode |-
75	2	adantr	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` L ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` L ) ) with typecode |-
76	75	raleqdv	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
77	75 76	raleqbidv	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
78	75 77	raleqbidv	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
79	70 74 78	3bitr3d	Could not format ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
80	79	pm5.32da	Could not format ( ph -> ( ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) with typecode |-
81		df-3an	Could not format ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) : No typesetting found for |- ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) with typecode |-
82		df-3an	Could not format ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
83	80 81 82	3bitr4g	Could not format ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) with typecode |-
84	1 2 3	ablpropd	$$⊢\phi \to \left(K\in \mathrm{Abel}\leftrightarrow L\in \mathrm{Abel}\right)$$
85		fvexd	$$⊢\phi \to {\mathrm{mulGrp}}_K\in \mathrm{V}$$
86		fvexd	$$⊢\phi \to {\mathrm{mulGrp}}_L\in \mathrm{V}$$
87	29	a1i	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
88		eqid	$$⊢{\mathrm{mulGrp}}_L={\mathrm{mulGrp}}_L$$
89		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
90	88 89	mgpbas	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_{{\mathrm{mulGrp}}_L}$$
91	2 90	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{mulGrp}}_L}$$
92	1 91	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_L}$$
93	4	ex	$$⊢\phi \to \left(\left(x\in B\wedge y\in B\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y\right)$$
94	1	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_K\right)$$
95	1	eleq2d	$$⊢\phi \to \left(y\in B\leftrightarrow y\in {\mathrm{Base}}_K\right)$$
96	94 95	anbi12d	$$⊢\phi \to \left(\left(x\in B\wedge y\in B\right)\leftrightarrow \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)$$
97	96	bicomd	$$⊢\phi \to \left(\left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\leftrightarrow \left(x\in B\wedge y\in B\right)\right)$$
98	31	a1i	$$⊢\phi \to {\cdot }_K={+}_{{\mathrm{mulGrp}}_K}$$
99	98	eqcomd	$$⊢\phi \to {+}_{{\mathrm{mulGrp}}_K}={\cdot }_K$$
100	99	oveqd	$$⊢\phi \to x{+}_{{\mathrm{mulGrp}}_K}y=x{\cdot }_{K}y$$
101		eqid	$$⊢{\cdot }_L={\cdot }_L$$
102	88 101	mgpplusg	$$⊢{\cdot }_L={+}_{{\mathrm{mulGrp}}_L}$$
103	102	a1i	$$⊢\phi \to {\cdot }_L={+}_{{\mathrm{mulGrp}}_L}$$
104	103	eqcomd	$$⊢\phi \to {+}_{{\mathrm{mulGrp}}_L}={\cdot }_L$$
105	104	oveqd	$$⊢\phi \to x{+}_{{\mathrm{mulGrp}}_L}y=x{\cdot }_{L}y$$
106	100 105	eqeq12d	$$⊢\phi \to \left(x{+}_{{\mathrm{mulGrp}}_K}y=x{+}_{{\mathrm{mulGrp}}_L}y\leftrightarrow x{\cdot }_{K}y=x{\cdot }_{L}y\right)$$
107	93 97 106	3imtr4d	$$⊢\phi \to \left(\left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\to x{+}_{{\mathrm{mulGrp}}_K}y=x{+}_{{\mathrm{mulGrp}}_L}y\right)$$
108	107	imp	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{+}_{{\mathrm{mulGrp}}_K}y=x{+}_{{\mathrm{mulGrp}}_L}y$$
109	85 86 87 92 108	sgrppropd	Could not format ( ph -> ( ( mulGrp ` K ) e. Smgrp <-> ( mulGrp ` L ) e. Smgrp ) ) : No typesetting found for |- ( ph -> ( ( mulGrp ` K ) e. Smgrp <-> ( mulGrp ` L ) e. Smgrp ) ) with typecode |-
110	84 109	3anbi12d	Could not format ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ ( mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ ( mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) with typecode |-
111	83 110	bitrd	Could not format ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( L e. Abel /\ ( mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( L e. Abel /\ ( mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) with typecode |-
112	14 28 15 30	isrng	Could not format ( K e. Rng <-> ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) : No typesetting found for |- ( K e. Rng <-> ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) ) with typecode |-
113		eqid	$$⊢{+}_L={+}_L$$
114	89 88 113 101	isrng	Could not format ( L e. Rng <-> ( L e. Abel /\ ( mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) : No typesetting found for |- ( L e. Rng <-> ( L e. Abel /\ ( mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) with typecode |-
115	111 112 114	3bitr4g	$$⊢\phi \to \left(K\in \mathrm{Rng}\leftrightarrow L\in \mathrm{Rng}\right)$$