Theorem grpsubfvalALT

Description: Shorter proof of grpsubfval using ax-rep . (Contributed by NM, 31-Mar-2014) (Revised by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 19-Feb-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	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	grpsubfvalALT	$$⊢\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	16 16	mpoex	$$⊢\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)\in \mathrm{V}$$
18	14 15 17	fvmpt	$$⊢G\in \mathrm{V}\to {-}_G=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
19	4 18	syl5eq	$$⊢G\in \mathrm{V}\to \underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
20		fvprc	$$⊢\neg G\in \mathrm{V}\to {-}_G=\varnothing$$
21	4 20	syl5eq	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{-}=\varnothing$$
22		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
23	1 22	syl5eq	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
24	23	olcd	$$⊢\neg G\in \mathrm{V}\to \left(B=\varnothing \vee B=\varnothing \right)$$
25		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$$
26	24 25	syl	$$⊢\neg G\in \mathrm{V}\to \left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)=\varnothing$$
27	21 26	eqtr4d	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$
28	19 27	pm2.61i	$$⊢\underset{\dot{}}{-}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}I\left(y\right)\right)$$