Theorem grpinvfvalALT

Description: Shorter proof of grpinvfval using ax-rep . (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpinvval.b	$$⊢B={\mathrm{Base}}_G$$
	grpinvval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinvval.o	$$⊢\underset{\dot{}}{0}=0_G$$
	grpinvval.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvfvalALT	$$⊢N=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpinvval.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinvval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpinvval.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		grpinvval.n	$$⊢N={inv}_g\left(G\right)$$
5		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
6	5 1	syl6eqr	$$⊢g=G\to {\mathrm{Base}}_g=B$$
7		fveq2	$$⊢g=G\to {+}_g={+}_G$$
8	7 2	syl6eqr	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
9	8	oveqd	$$⊢g=G\to y{+}_{g}x=y\underset{\dot{}}{+}x$$
10		fveq2	$$⊢g=G\to 0_g=0_G$$
11	10 3	syl6eqr	$$⊢g=G\to 0_g=\underset{\dot{}}{0}$$
12	9 11	eqeq12d	$$⊢g=G\to \left(y{+}_{g}x=0_g\leftrightarrow y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
13	6 12	riotaeqbidv	$$⊢g=G\to \left(\iota y\in {\mathrm{Base}}_g|y{+}_{g}x=0_g\right)=\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
14	6 13	mpteq12dv	$$⊢g=G\to \left(x\in {\mathrm{Base}}_g⟼\left(\iota y\in {\mathrm{Base}}_g|y{+}_{g}x=0_g\right)\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
15		df-minusg	$$⊢{inv}_g=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼\left(\iota y\in {\mathrm{Base}}_g|y{+}_{g}x=0_g\right)\right)\right)$$
16	14 15 1	mptfvmpt	$$⊢G\in \mathrm{V}\to {inv}_g\left(G\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
17		fvprc	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(G\right)=\varnothing$$
18		mpt0	$$⊢\left(x\in \varnothing ⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)=\varnothing$$
19	17 18	syl6eqr	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(G\right)=\left(x\in \varnothing ⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
20		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
21	1 20	syl5eq	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
22	21	mpteq1d	$$⊢\neg G\in \mathrm{V}\to \left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)=\left(x\in \varnothing ⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
23	19 22	eqtr4d	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(G\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
24	16 23	pm2.61i	$$⊢{inv}_g\left(G\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
25	4 24	eqtri	$$⊢N=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$