Theorem grpinvpropd

Description: If two structures have the same group components (properties), they have the same group inversion function. (Contributed by Mario Carneiro, 27-Nov-2014) (Revised by Stefan O'Rear, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		grpinvpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		grpinvpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		grpinvpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4	1 2 3	grpidpropd	$$⊢\phi \to 0_K=0_L$$
5	4	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to 0_K=0_L$$
6	3 5	eqeq12d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x{+}_{K}y=0_K\leftrightarrow x{+}_{L}y=0_L\right)$$
7	6	anass1rs	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge x\in B\right)\to \left(x{+}_{K}y=0_K\leftrightarrow x{+}_{L}y=0_L\right)$$
8	7	riotabidva	$$⊢\left(\phi \wedge y\in B\right)\to \left(\iota x\in B|x{+}_{K}y=0_K\right)=\left(\iota x\in B|x{+}_{L}y=0_L\right)$$
9	8	mpteq2dva	$$⊢\phi \to \left(y\in B⟼\left(\iota x\in B|x{+}_{K}y=0_K\right)\right)=\left(y\in B⟼\left(\iota x\in B|x{+}_{L}y=0_L\right)\right)$$
10	1	riotaeqdv	$$⊢\phi \to \left(\iota x\in B|x{+}_{K}y=0_K\right)=\left(\iota x\in {\mathrm{Base}}_K|x{+}_{K}y=0_K\right)$$
11	1 10	mpteq12dv	$$⊢\phi \to \left(y\in B⟼\left(\iota x\in B|x{+}_{K}y=0_K\right)\right)=\left(y\in {\mathrm{Base}}_K⟼\left(\iota x\in {\mathrm{Base}}_K|x{+}_{K}y=0_K\right)\right)$$
12	2	riotaeqdv	$$⊢\phi \to \left(\iota x\in B|x{+}_{L}y=0_L\right)=\left(\iota x\in {\mathrm{Base}}_L|x{+}_{L}y=0_L\right)$$
13	2 12	mpteq12dv	$$⊢\phi \to \left(y\in B⟼\left(\iota x\in B|x{+}_{L}y=0_L\right)\right)=\left(y\in {\mathrm{Base}}_L⟼\left(\iota x\in {\mathrm{Base}}_L|x{+}_{L}y=0_L\right)\right)$$
14	9 11 13	3eqtr3d	$$⊢\phi \to \left(y\in {\mathrm{Base}}_K⟼\left(\iota x\in {\mathrm{Base}}_K|x{+}_{K}y=0_K\right)\right)=\left(y\in {\mathrm{Base}}_L⟼\left(\iota x\in {\mathrm{Base}}_L|x{+}_{L}y=0_L\right)\right)$$
15		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
16		eqid	$$⊢{+}_K={+}_K$$
17		eqid	$$⊢0_K=0_K$$
18		eqid	$$⊢{inv}_g\left(K\right)={inv}_g\left(K\right)$$
19	15 16 17 18	grpinvfval	$$⊢{inv}_g\left(K\right)=\left(y\in {\mathrm{Base}}_K⟼\left(\iota x\in {\mathrm{Base}}_K|x{+}_{K}y=0_K\right)\right)$$
20		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
21		eqid	$$⊢{+}_L={+}_L$$
22		eqid	$$⊢0_L=0_L$$
23		eqid	$$⊢{inv}_g\left(L\right)={inv}_g\left(L\right)$$
24	20 21 22 23	grpinvfval	$$⊢{inv}_g\left(L\right)=\left(y\in {\mathrm{Base}}_L⟼\left(\iota x\in {\mathrm{Base}}_L|x{+}_{L}y=0_L\right)\right)$$
25	14 19 24	3eqtr4g	$$⊢\phi \to {inv}_g\left(K\right)={inv}_g\left(L\right)$$