Theorem grpsubfval

Description: Group subtraction (division) operation. For a shorter proof using ax-rep , see grpsubfvalALT . (Contributed by NM, 31-Mar-2014) (Revised by Stefan O'Rear, 27-Mar-2015) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023) (Proof shortened by AV, 19-Feb-2024)

	Ref	Expression
Hypotheses	grpsubval.b	$$⊢B={\mathrm{Base}}_G$$
	grpsubval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpsubval.i	$$⊢I={inv}_g\left(G\right)$$
	grpsubval.m	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	grpsubfval	$$⊢\underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpsubval.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpsubval.i	$$⊢I={inv}_g\left(G\right)$$
4		grpsubval.m	$$⊢\underset{\dot{}}{-}={-}_G$$
5		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
6	5 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=B$$
7		fveq2	$$⊢g=G\to {+}_g={+}_G$$
8	7 2	eqtr4di	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
9		eqidd	$$⊢g=G\to x=x$$
10		fveq2	$$⊢g=G\to {inv}_g\left(g\right)={inv}_g\left(G\right)$$
11	10 3	eqtr4di	$$⊢g=G\to {inv}_g\left(g\right)=I$$
12	11	fveq1d	$$⊢g=G\to {inv}_g\left(g\right)\left(y\right)=I\left(y\right)$$
13	8 9 12	oveq123d	$$⊢g=G\to x{+}_g{inv}_g\left(g\right)\left(y\right)=x\underset{\dot{}}{+}I\left(y\right)$$
14	6 6 13	mpoeq123dv	$$⊢g=G\to \left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_g{inv}_g\left(g\right)\left(y\right)\right)=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
15		df-sbg	$$⊢{-}_{𝑔}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_g{inv}_g\left(g\right)\left(y\right)\right)\right)$$
16	1	fvexi	$$⊢B\in \mathrm{V}$$
17	2	fvexi	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
18	17	rnex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\in \mathrm{V}$$
19		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
20	18 19	unex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\in \mathrm{V}$$
21		df-ov	$$⊢x\underset{\dot{}}{+}I\left(y\right)=\underset{\dot{}}{+}\left(⟨x,I\left(y\right)⟩\right)$$
22		fvrn0	$$⊢\underset{\dot{}}{+}\left(⟨x,I\left(y\right)⟩\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
23	21 22	eqeltri	$$⊢x\underset{\dot{}}{+}I\left(y\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
24	23	rgen2w	$$⊢\forall x\in B\forall y\in Bx\underset{\dot{}}{+}I\left(y\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
25	16 16 20 24	mpoexw	$$⊢\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)\in \mathrm{V}$$
26	14 15 25	fvmpt	$$⊢G\in \mathrm{V}\to {-}_G=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
27	4 26	eqtrid	$$⊢G\in \mathrm{V}\to \underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
28		fvprc	$$⊢\neg G\in \mathrm{V}\to {-}_G=\varnothing$$
29	4 28	eqtrid	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{-}=\varnothing$$
30		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
31	1 30	eqtrid	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
32	31	olcd	$$⊢\neg G\in \mathrm{V}\to \left(B=\varnothing \vee B=\varnothing \right)$$
33		0mpo0	$$⊢\left(B=\varnothing \vee B=\varnothing \right)\to \left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)=\varnothing$$
34	32 33	syl	$$⊢\neg G\in \mathrm{V}\to \left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)=\varnothing$$
35	29 34	eqtr4d	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
36	27 35	pm2.61i	$$⊢\underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$