Theorem mulgfvalALT

Description: Shorter proof of mulgfval using ax-rep . (Contributed by Mario Carneiro, 11-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mulgval.b	$$⊢B={\mathrm{Base}}_G$$
	mulgval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mulgval.o	$$⊢\underset{\dot{}}{0}=0_G$$
	mulgval.i	$$⊢I={inv}_g\left(G\right)$$
	mulgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulgfvalALT	$$⊢\underset{\dot{}}{·}=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulgval.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mulgval.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		mulgval.i	$$⊢I={inv}_g\left(G\right)$$
5		mulgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
6		eqidd	$$⊢w=G\to \mathbb{Z}=\mathbb{Z}$$
7		fveq2	$$⊢w=G\to {\mathrm{Base}}_w={\mathrm{Base}}_G$$
8	7 1	syl6eqr	$$⊢w=G\to {\mathrm{Base}}_w=B$$
9		fveq2	$$⊢w=G\to 0_w=0_G$$
10	9 3	syl6eqr	$$⊢w=G\to 0_w=\underset{\dot{}}{0}$$
11		seqex	$$⊢seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\in \mathrm{V}$$
12	11	a1i	$$⊢w=G\to seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\in \mathrm{V}$$
13		id	$$⊢s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\to s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)$$
14		fveq2	$$⊢w=G\to {+}_w={+}_G$$
15	14 2	syl6eqr	$$⊢w=G\to {+}_w=\underset{\dot{}}{+}$$
16	15	seqeq2d	$$⊢w=G\to seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)$$
17	13 16	sylan9eqr	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to s=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)$$
18	17	fveq1d	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to s\left(n\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)$$
19		simpl	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to w=G$$
20	19	fveq2d	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to {inv}_g\left(w\right)={inv}_g\left(G\right)$$
21	20 4	syl6eqr	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to {inv}_g\left(w\right)=I$$
22	17	fveq1d	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to s\left(-n\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)$$
23	21 22	fveq12d	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to {inv}_g\left(w\right)\left(s\left(-n\right)\right)=I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)$$
24	18 23	ifeq12d	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to if\left(0<n,s\left(n\right),{inv}_g\left(w\right)\left(s\left(-n\right)\right)\right)=if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)$$
25	12 24	csbied	$$⊢w=G\to ⦋seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(w\right)\left(s\left(-n\right)\right)\right)=if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)$$
26	10 25	ifeq12d	$$⊢w=G\to if\left(n=0,0_w,⦋seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(w\right)\left(s\left(-n\right)\right)\right)\right)=if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)$$
27	6 8 26	mpoeq123dv	$$⊢w=G\to \left(n\in \mathbb{Z},x\in {\mathrm{Base}}_w⟼if\left(n=0,0_w,⦋seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(w\right)\left(s\left(-n\right)\right)\right)\right)\right)=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$
28		df-mulg	$$⊢{\mathrm{\cdot }}_{𝑔}=\left(w\in \mathrm{V}⟼\left(n\in \mathbb{Z},x\in {\mathrm{Base}}_w⟼if\left(n=0,0_w,⦋seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(w\right)\left(s\left(-n\right)\right)\right)\right)\right)\right)$$
29		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
30	1	fvexi	$$⊢B\in \mathrm{V}$$
31	29 30	mpoex	$$⊢\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)\in \mathrm{V}$$
32	27 28 31	fvmpt	$$⊢G\in \mathrm{V}\to {\cdot }_G=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$
33		fvprc	$$⊢\neg G\in \mathrm{V}\to {\cdot }_G=\varnothing$$
34		eqid	$$⊢\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$
35	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
36		fvex	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \mathrm{V}$$
37		fvex	$$⊢I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\in \mathrm{V}$$
38	36 37	ifex	$$⊢if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\in \mathrm{V}$$
39	35 38	ifex	$$⊢if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\in \mathrm{V}$$
40	34 39	fnmpoi	$$⊢\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)Fn\left(\mathbb{Z}\times B\right)$$
41		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
42	1 41	syl5eq	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
43	42	xpeq2d	$$⊢\neg G\in \mathrm{V}\to \mathbb{Z}\times B=\mathbb{Z}\times \varnothing$$
44		xp0	$$⊢\mathbb{Z}\times \varnothing =\varnothing$$
45	43 44	syl6eq	$$⊢\neg G\in \mathrm{V}\to \mathbb{Z}\times B=\varnothing$$
46	45	fneq2d	$$⊢\neg G\in \mathrm{V}\to \left(\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)Fn\left(\mathbb{Z}\times B\right)\leftrightarrow \left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)Fn\varnothing \right)$$
47	40 46	mpbii	$$⊢\neg G\in \mathrm{V}\to \left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)Fn\varnothing$$
48		fn0	$$⊢\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)Fn\varnothing \leftrightarrow \left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)=\varnothing$$
49	47 48	sylib	$$⊢\neg G\in \mathrm{V}\to \left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)=\varnothing$$
50	33 49	eqtr4d	$$⊢\neg G\in \mathrm{V}\to {\cdot }_G=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$
51	32 50	pm2.61i	$$⊢{\cdot }_G=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$
52	5 51	eqtri	$$⊢\underset{\dot{}}{·}=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$