Theorem mulgfval

Description: Group multiple (exponentiation) operation. For a shorter proof using ax-rep , see mulgfvalALT . (Contributed by Mario Carneiro, 11-Dec-2014) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023)

	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	mulgfval	$$⊢\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		fvex	$$⊢{+}_w\in \mathrm{V}$$
12		1z	$$⊢1\in \mathbb{Z}$$
13	11 12	seqexw	$$⊢seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\in \mathrm{V}$$
14	13	a1i	$$⊢w=G\to seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\in \mathrm{V}$$
15		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)$$
16		fveq2	$$⊢w=G\to {+}_w={+}_G$$
17	16 2	syl6eqr	$$⊢w=G\to {+}_w=\underset{\dot{}}{+}$$
18	17	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)$$
19	15 18	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)$$
20	19	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)$$
21		simpl	$$⊢\left(w=G\wedge s=seq1\left({+}_w,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\right)\to w=G$$
22	21	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)$$
23	22 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$$
24	19	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)$$
25	23 24	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)$$
26	20 25	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)$$
27	14 26	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)$$
28	10 27	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)$$
29	6 8 28	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)$$
30		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)$$
31		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
32	1	fvexi	$$⊢B\in \mathrm{V}$$
33		snex	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
34	2	fvexi	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
35	34	rnex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\in \mathrm{V}$$
36	35 32	unex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup B\in \mathrm{V}$$
37	4	fvexi	$$⊢I\in \mathrm{V}$$
38	37	rnex	$$⊢\mathrm{ran}I\in \mathrm{V}$$
39		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
40	38 39	unex	$$⊢\mathrm{ran}I\cup \left\{\varnothing \right\}\in \mathrm{V}$$
41	36 40	unex	$$⊢\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\in \mathrm{V}$$
42	33 41	unex	$$⊢\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\in \mathrm{V}$$
43		ssun1	$$⊢\left\{\underset{\dot{}}{0}\right\}\subseteq \left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)$$
44	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
45	44	snid	$$⊢\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
46	43 45	sselii	$$⊢\underset{\dot{}}{0}\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
47	46	a1i	$$⊢\left(n\in \mathbb{Z}\wedge x\in B\right)\to \underset{\dot{}}{0}\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
48		ssun2	$$⊢B\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup B$$
49		ssun1	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup B\subseteq \left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)$$
50	48 49	sstri	$$⊢B\subseteq \left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)$$
51		ssun2	$$⊢\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\subseteq \left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)$$
52	50 51	sstri	$$⊢B\subseteq \left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)$$
53		fveq2	$$⊢n=1\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(1\right)$$
54	53	adantl	$$⊢\left(x\in B\wedge n=1\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(1\right)$$
55		seq1	$$⊢1\in \mathbb{Z}\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(1\right)=\left(\mathbb{N}\times \left\{x\right\}\right)\left(1\right)$$
56	12 55	ax-mp	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(1\right)=\left(\mathbb{N}\times \left\{x\right\}\right)\left(1\right)$$
57		1nn	$$⊢1\in \mathbb{N}$$
58		vex	$$⊢x\in \mathrm{V}$$
59	58	fvconst2	$$⊢1\in \mathbb{N}\to \left(\mathbb{N}\times \left\{x\right\}\right)\left(1\right)=x$$
60	57 59	ax-mp	$$⊢\left(\mathbb{N}\times \left\{x\right\}\right)\left(1\right)=x$$
61	60	eleq1i	$$⊢\left(\mathbb{N}\times \left\{x\right\}\right)\left(1\right)\in B\leftrightarrow x\in B$$
62	61	biimpri	$$⊢x\in B\to \left(\mathbb{N}\times \left\{x\right\}\right)\left(1\right)\in B$$
63	56 62	eqeltrid	$$⊢x\in B\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(1\right)\in B$$
64	63	adantr	$$⊢\left(x\in B\wedge n=1\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(1\right)\in B$$
65	54 64	eqeltrd	$$⊢\left(x\in B\wedge n=1\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in B$$
66	52 65	sseldi	$$⊢\left(x\in B\wedge n=1\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
67	66	ad4ant24	$$⊢\left(\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge n\in {\mathbb{Z}}_{\ge 1}\right)\wedge n=1\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
68		zcn	$$⊢n\in \mathbb{Z}\to n\in ℂ$$
69		npcan1	$$⊢n\in ℂ\to n-1+1=n$$
70	68 69	syl	$$⊢n\in \mathbb{Z}\to n-1+1=n$$
71	70	fveq2d	$$⊢n\in \mathbb{Z}\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1+1\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)$$
72	71	adantr	$$⊢\left(n\in \mathbb{Z}\wedge n-1\in {\mathbb{Z}}_{\ge 1}\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1+1\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)$$
73		seqp1	$$⊢n-1\in {\mathbb{Z}}_{\ge 1}\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1+1\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1\right)\underset{\dot{}}{+}\left(\mathbb{N}\times \left\{x\right\}\right)\left(n-1+1\right)$$
74		ssun1	$$⊢\mathrm{ran}\underset{\dot{}}{+}\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup B$$
75		ssun2	$$⊢\left\{\varnothing \right\}\subseteq \mathrm{ran}I\cup \left\{\varnothing \right\}$$
76		unss12	$$⊢\left(\mathrm{ran}\underset{\dot{}}{+}\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup B\wedge \left\{\varnothing \right\}\subseteq \mathrm{ran}I\cup \left\{\varnothing \right\}\right)\to \mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\subseteq \left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)$$
77	74 75 76	mp2an	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\subseteq \left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)$$
78	77 51	sstri	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\subseteq \left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)$$
79		df-ov	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1\right)\underset{\dot{}}{+}\left(\mathbb{N}\times \left\{x\right\}\right)\left(n-1+1\right)=\underset{\dot{}}{+}\left(⟨seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1\right),\left(\mathbb{N}\times \left\{x\right\}\right)\left(n-1+1\right)⟩\right)$$
80		fvrn0	$$⊢\underset{\dot{}}{+}\left(⟨seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1\right),\left(\mathbb{N}\times \left\{x\right\}\right)\left(n-1+1\right)⟩\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
81	79 80	eqeltri	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1\right)\underset{\dot{}}{+}\left(\mathbb{N}\times \left\{x\right\}\right)\left(n-1+1\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
82	78 81	sselii	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1\right)\underset{\dot{}}{+}\left(\mathbb{N}\times \left\{x\right\}\right)\left(n-1+1\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
83	73 82	eqeltrdi	$$⊢n-1\in {\mathbb{Z}}_{\ge 1}\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1+1\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
84	83	adantl	$$⊢\left(n\in \mathbb{Z}\wedge n-1\in {\mathbb{Z}}_{\ge 1}\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n-1+1\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
85	72 84	eqeltrrd	$$⊢\left(n\in \mathbb{Z}\wedge n-1\in {\mathbb{Z}}_{\ge 1}\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
86	85	ad4ant14	$$⊢\left(\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge n\in {\mathbb{Z}}_{\ge 1}\right)\wedge n-1\in {\mathbb{Z}}_{\ge 1}\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
87		uzm1	$$⊢n\in {\mathbb{Z}}_{\ge 1}\to \left(n=1\vee n-1\in {\mathbb{Z}}_{\ge 1}\right)$$
88	87	adantl	$$⊢\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge n\in {\mathbb{Z}}_{\ge 1}\right)\to \left(n=1\vee n-1\in {\mathbb{Z}}_{\ge 1}\right)$$
89	67 86 88	mpjaodan	$$⊢\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge n\in {\mathbb{Z}}_{\ge 1}\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
90		simpr	$$⊢\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge \neg n\in {\mathbb{Z}}_{\ge 1}\right)\to \neg n\in {\mathbb{Z}}_{\ge 1}$$
91		seqfn	$$⊢1\in \mathbb{Z}\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)Fn{\mathbb{Z}}_{\ge 1}$$
92	12 91	ax-mp	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)Fn{\mathbb{Z}}_{\ge 1}$$
93		fndm	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)Fn{\mathbb{Z}}_{\ge 1}\to \mathrm{dom}seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)={\mathbb{Z}}_{\ge 1}$$
94	92 93	ax-mp	$$⊢\mathrm{dom}seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)={\mathbb{Z}}_{\ge 1}$$
95	94	eleq2i	$$⊢n\in \mathrm{dom}seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\leftrightarrow n\in {\mathbb{Z}}_{\ge 1}$$
96	90 95	sylnibr	$$⊢\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge \neg n\in {\mathbb{Z}}_{\ge 1}\right)\to \neg n\in \mathrm{dom}seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)$$
97		ndmfv	$$⊢\neg n\in \mathrm{dom}seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)=\varnothing$$
98	96 97	syl	$$⊢\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge \neg n\in {\mathbb{Z}}_{\ge 1}\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)=\varnothing$$
99		ssun2	$$⊢\mathrm{ran}I\cup \left\{\varnothing \right\}\subseteq \left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)$$
100	75 99	sstri	$$⊢\left\{\varnothing \right\}\subseteq \left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)$$
101	100 51	sstri	$$⊢\left\{\varnothing \right\}\subseteq \left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)$$
102		0ex	$$⊢\varnothing \in \mathrm{V}$$
103	102	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
104	101 103	sselii	$$⊢\varnothing \in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
105	104	a1i	$$⊢\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge \neg n\in {\mathbb{Z}}_{\ge 1}\right)\to \varnothing \in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
106	98 105	eqeltrd	$$⊢\left(\left(n\in \mathbb{Z}\wedge x\in B\right)\wedge \neg n\in {\mathbb{Z}}_{\ge 1}\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
107	89 106	pm2.61dan	$$⊢\left(n\in \mathbb{Z}\wedge x\in B\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
108	99 51	sstri	$$⊢\mathrm{ran}I\cup \left\{\varnothing \right\}\subseteq \left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)$$
109		fvrn0	$$⊢I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\in \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)$$
110	108 109	sselii	$$⊢I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
111	110	a1i	$$⊢\left(n\in \mathbb{Z}\wedge x\in B\right)\to I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\in \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
112	107 111	ifcld	$$⊢\left(n\in \mathbb{Z}\wedge x\in B\right)\to 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 \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
113	47 112	ifcld	$$⊢\left(n\in \mathbb{Z}\wedge x\in B\right)\to 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 \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
114	113	rgen2	$$⊢\forall n\in \mathbb{Z}\forall x\in Bif\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 \left(\left\{\underset{\dot{}}{0}\right\}\cup \left(\left(\mathrm{ran}\underset{\dot{}}{+}\cup B\right)\cup \left(\mathrm{ran}I\cup \left\{\varnothing \right\}\right)\right)\right)$$
115	31 32 42 114	mpoexw	$$⊢\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}$$
116	29 30 115	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)$$
117		fvprc	$$⊢\neg G\in \mathrm{V}\to {\cdot }_G=\varnothing$$
118		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)$$
119		fvex	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \mathrm{V}$$
120		fvex	$$⊢I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\in \mathrm{V}$$
121	119 120	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}$$
122	44 121	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}$$
123	118 122	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)$$
124		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
125	1 124	syl5eq	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
126	125	xpeq2d	$$⊢\neg G\in \mathrm{V}\to \mathbb{Z}\times B=\mathbb{Z}\times \varnothing$$
127		xp0	$$⊢\mathbb{Z}\times \varnothing =\varnothing$$
128	126 127	syl6eq	$$⊢\neg G\in \mathrm{V}\to \mathbb{Z}\times B=\varnothing$$
129	128	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)$$
130	123 129	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$$
131		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$$
132	130 131	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$$
133	117 132	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)$$
134	116 133	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)$$
135	5 134	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)$$