Theorem plusffval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	plusffval.1	$$⊢B={\mathrm{Base}}_G$$
	plusffval.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	plusffval.3	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
Assertion	plusffval	$$⊢\underset{\dot{}}{⨣}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		plusffval.1	$$⊢B={\mathrm{Base}}_G$$
2		plusffval.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		plusffval.3	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
4		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
5	4 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=B$$
6		fveq2	$$⊢g=G\to {+}_g={+}_G$$
7	6 2	eqtr4di	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
8	7	oveqd	$$⊢g=G\to x{+}_{g}y=x\underset{\dot{}}{+}y$$
9	5 5 8	mpoeq123dv	$$⊢g=G\to \left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_{g}y\right)=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
10		df-plusf	$$⊢{+}_{𝑓}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_{g}y\right)\right)$$
11	1	fvexi	$$⊢B\in \mathrm{V}$$
12	2	fvexi	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
13	12	rnex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\in \mathrm{V}$$
14		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
15	13 14	unex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\in \mathrm{V}$$
16		df-ov	$$⊢x\underset{\dot{}}{+}y=\underset{\dot{}}{+}\left(⟨x,y⟩\right)$$
17		fvrn0	$$⊢\underset{\dot{}}{+}\left(⟨x,y⟩\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
18	16 17	eqeltri	$$⊢x\underset{\dot{}}{+}y\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
19	18	rgen2w	$$⊢\forall x\in B\forall y\in Bx\underset{\dot{}}{+}y\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
20	11 11 15 19	mpoexw	$$⊢\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)\in \mathrm{V}$$
21	9 10 20	fvmpt	$$⊢G\in \mathrm{V}\to {+}_{𝑓}\left(G\right)=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
22		fvprc	$$⊢\neg G\in \mathrm{V}\to {+}_{𝑓}\left(G\right)=\varnothing$$
23		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
24	1 23	syl5eq	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
25	24	olcd	$$⊢\neg G\in \mathrm{V}\to \left(B=\varnothing \vee B=\varnothing \right)$$
26		0mpo0	$$⊢\left(B=\varnothing \vee B=\varnothing \right)\to \left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)=\varnothing$$
27	25 26	syl	$$⊢\neg G\in \mathrm{V}\to \left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)=\varnothing$$
28	22 27	eqtr4d	$$⊢\neg G\in \mathrm{V}\to {+}_{𝑓}\left(G\right)=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
29	21 28	pm2.61i	$$⊢{+}_{𝑓}\left(G\right)=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
30	3 29	eqtri	$$⊢\underset{\dot{}}{⨣}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$