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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulgval.p	⊢ + = ( +_g ‘ 𝐺 )
	mulgval.o	⊢ 0 = ( 0_g ‘ 𝐺 )
	mulgval.i	⊢ 𝐼 = ( inv_g ‘ 𝐺 )
	mulgval.t	⊢ · = ( ._g ‘ 𝐺 )
Assertion	mulgfval	⊢ · = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulgval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulgval.p	⊢ + = ( +_g ‘ 𝐺 )
3		mulgval.o	⊢ 0 = ( 0_g ‘ 𝐺 )
4		mulgval.i	⊢ 𝐼 = ( inv_g ‘ 𝐺 )
5		mulgval.t	⊢ · = ( ._g ‘ 𝐺 )
6		eqidd	⊢ ( 𝑤 = 𝐺 → ℤ = ℤ )
7		fveq2	⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐺 ) )
8	7 1	eqtr4di	⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = 𝐵 )
9		fveq2	⊢ ( 𝑤 = 𝐺 → ( 0_g ‘ 𝑤 ) = ( 0_g ‘ 𝐺 ) )
10	9 3	eqtr4di	⊢ ( 𝑤 = 𝐺 → ( 0_g ‘ 𝑤 ) = 0 )
11		fvex	⊢ ( +_g ‘ 𝑤 ) ∈ V
12		1z	⊢ 1 ∈ ℤ
13	11 12	seqexw	⊢ seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ∈ V
14	13	a1i	⊢ ( 𝑤 = 𝐺 → seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ∈ V )
15		id	⊢ ( 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) → 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) )
16		fveq2	⊢ ( 𝑤 = 𝐺 → ( +_g ‘ 𝑤 ) = ( +_g ‘ 𝐺 ) )
17	16 2	eqtr4di	⊢ ( 𝑤 = 𝐺 → ( +_g ‘ 𝑤 ) = + )
18	17	seqeq2d	⊢ ( 𝑤 = 𝐺 → seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) = seq 1 ( + , ( ℕ × { 𝑥 } ) ) )
19	15 18	sylan9eqr	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → 𝑠 = seq 1 ( + , ( ℕ × { 𝑥 } ) ) )
20	19	fveq1d	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( 𝑠 ‘ 𝑛 ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) )
21		simpl	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → 𝑤 = 𝐺 )
22	21	fveq2d	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( inv_g ‘ 𝑤 ) = ( inv_g ‘ 𝐺 ) )
23	22 4	eqtr4di	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( inv_g ‘ 𝑤 ) = 𝐼 )
24	19	fveq1d	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( 𝑠 ‘ - 𝑛 ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) )
25	23 24	fveq12d	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( ( inv_g ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) = ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) )
26	20 25	ifeq12d	⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( inv_g ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) = if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) )
27	14 26	csbied	⊢ ( 𝑤 = 𝐺 → ⦋ seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( inv_g ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) = if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) )
28	10 27	ifeq12d	⊢ ( 𝑤 = 𝐺 → if ( 𝑛 = 0 , ( 0_g ‘ 𝑤 ) , ⦋ seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( inv_g ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) = if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )
29	6 8 28	mpoeq123dv	⊢ ( 𝑤 = 𝐺 → ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ if ( 𝑛 = 0 , ( 0_g ‘ 𝑤 ) , ⦋ seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( inv_g ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) )
30		df-mulg	⊢ ._g = ( 𝑤 ∈ V ↦ ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ if ( 𝑛 = 0 , ( 0_g ‘ 𝑤 ) , ⦋ seq 1 ( ( +_g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( inv_g ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) )
31		zex	⊢ ℤ ∈ V
32	1	fvexi	⊢ 𝐵 ∈ V
33		snex	⊢ { 0 } ∈ V
34	2	fvexi	⊢ + ∈ V
35	34	rnex	⊢ ran + ∈ V
36	35 32	unex	⊢ ( ran + ∪ 𝐵 ) ∈ V
37	4	fvexi	⊢ 𝐼 ∈ V
38	37	rnex	⊢ ran 𝐼 ∈ V
39		p0ex	⊢ { ∅ } ∈ V
40	38 39	unex	⊢ ( ran 𝐼 ∪ { ∅ } ) ∈ V
41	36 40	unex	⊢ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ∈ V
42	33 41	unex	⊢ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) ∈ V
43		ssun1	⊢ { 0 } ⊆ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
44	3	fvexi	⊢ 0 ∈ V
45	44	snid	⊢ 0 ∈ { 0 }
46	43 45	sselii	⊢ 0 ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
47	46	a1i	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → 0 ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
48		ssun2	⊢ 𝐵 ⊆ ( ran + ∪ 𝐵 )
49		ssun1	⊢ ( ran + ∪ 𝐵 ) ⊆ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) )
50	48 49	sstri	⊢ 𝐵 ⊆ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) )
51		ssun2	⊢ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ⊆ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
52	50 51	sstri	⊢ 𝐵 ⊆ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
53		fveq2	⊢ ( 𝑛 = 1 → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 1 ) )
54	53	adantl	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑛 = 1 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 1 ) )
55		seq1	⊢ ( 1 ∈ ℤ → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 1 ) = ( ( ℕ × { 𝑥 } ) ‘ 1 ) )
56	12 55	ax-mp	⊢ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 1 ) = ( ( ℕ × { 𝑥 } ) ‘ 1 )
57		1nn	⊢ 1 ∈ ℕ
58		vex	⊢ 𝑥 ∈ V
59	58	fvconst2	⊢ ( 1 ∈ ℕ → ( ( ℕ × { 𝑥 } ) ‘ 1 ) = 𝑥 )
60	57 59	ax-mp	⊢ ( ( ℕ × { 𝑥 } ) ‘ 1 ) = 𝑥
61	60	eleq1i	⊢ ( ( ( ℕ × { 𝑥 } ) ‘ 1 ) ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 )
62	61	biimpri	⊢ ( 𝑥 ∈ 𝐵 → ( ( ℕ × { 𝑥 } ) ‘ 1 ) ∈ 𝐵 )
63	56 62	eqeltrid	⊢ ( 𝑥 ∈ 𝐵 → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 1 ) ∈ 𝐵 )
64	63	adantr	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑛 = 1 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 1 ) ∈ 𝐵 )
65	54 64	eqeltrd	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑛 = 1 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ 𝐵 )
66	52 65	sselid	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑛 = 1 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
67	66	ad4ant24	⊢ ( ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) ∧ 𝑛 = 1 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
68		zcn	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
69		npcan1	⊢ ( 𝑛 ∈ ℂ → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
70	68 69	syl	⊢ ( 𝑛 ∈ ℤ → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
71	70	fveq2d	⊢ ( 𝑛 ∈ ℤ → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) )
72	71	adantr	⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) )
73		seqp1	⊢ ( ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( 𝑛 − 1 ) ) + ( ( ℕ × { 𝑥 } ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) )
74		ssun1	⊢ ran + ⊆ ( ran + ∪ 𝐵 )
75		ssun2	⊢ { ∅ } ⊆ ( ran 𝐼 ∪ { ∅ } )
76		unss12	⊢ ( ( ran + ⊆ ( ran + ∪ 𝐵 ) ∧ { ∅ } ⊆ ( ran 𝐼 ∪ { ∅ } ) ) → ( ran + ∪ { ∅ } ) ⊆ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
77	74 75 76	mp2an	⊢ ( ran + ∪ { ∅ } ) ⊆ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) )
78	77 51	sstri	⊢ ( ran + ∪ { ∅ } ) ⊆ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
79		df-ov	⊢ ( ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( 𝑛 − 1 ) ) + ( ( ℕ × { 𝑥 } ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) = ( + ‘ ⟨ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( 𝑛 − 1 ) ) , ( ( ℕ × { 𝑥 } ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ⟩ )
80		fvrn0	⊢ ( + ‘ ⟨ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( 𝑛 − 1 ) ) , ( ( ℕ × { 𝑥 } ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ⟩ ) ∈ ( ran + ∪ { ∅ } )
81	79 80	eqeltri	⊢ ( ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( 𝑛 − 1 ) ) + ( ( ℕ × { 𝑥 } ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) ∈ ( ran + ∪ { ∅ } )
82	78 81	sselii	⊢ ( ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( 𝑛 − 1 ) ) + ( ( ℕ × { 𝑥 } ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
83	73 82	eqeltrdi	⊢ ( ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
84	83	adantl	⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ ( ( 𝑛 − 1 ) + 1 ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
85	72 84	eqeltrrd	⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
86	85	ad4ant14	⊢ ( ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) ∧ ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
87		uzm1	⊢ ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) → ( 𝑛 = 1 ∨ ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) ) )
88	87	adantl	⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) → ( 𝑛 = 1 ∨ ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ 1 ) ) )
89	67 86 88	mpjaodan	⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
90		simpr	⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) → ¬ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) )
91		seqfn	⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ℕ × { 𝑥 } ) ) Fn ( ℤ_≥ ‘ 1 ) )
92	12 91	ax-mp	⊢ seq 1 ( + , ( ℕ × { 𝑥 } ) ) Fn ( ℤ_≥ ‘ 1 )
93	92	fndmi	⊢ dom seq 1 ( + , ( ℕ × { 𝑥 } ) ) = ( ℤ_≥ ‘ 1 )
94	93	eleq2i	⊢ ( 𝑛 ∈ dom seq 1 ( + , ( ℕ × { 𝑥 } ) ) ↔ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) )
95	90 94	sylnibr	⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) → ¬ 𝑛 ∈ dom seq 1 ( + , ( ℕ × { 𝑥 } ) ) )
96		ndmfv	⊢ ( ¬ 𝑛 ∈ dom seq 1 ( + , ( ℕ × { 𝑥 } ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) = ∅ )
97	95 96	syl	⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) = ∅ )
98		ssun2	⊢ ( ran 𝐼 ∪ { ∅ } ) ⊆ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) )
99	75 98	sstri	⊢ { ∅ } ⊆ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) )
100	99 51	sstri	⊢ { ∅ } ⊆ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
101		0ex	⊢ ∅ ∈ V
102	101	snid	⊢ ∅ ∈ { ∅ }
103	100 102	sselii	⊢ ∅ ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
104	103	a1i	⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) → ∅ ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
105	97 104	eqeltrd	⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
106	89 105	pm2.61dan	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
107	98 51	sstri	⊢ ( ran 𝐼 ∪ { ∅ } ) ⊆ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
108		fvrn0	⊢ ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ∈ ( ran 𝐼 ∪ { ∅ } )
109	107 108	sselii	⊢ ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
110	109	a1i	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
111	106 110	ifcld	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
112	47 111	ifcld	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) ) )
113	112	rgen2	⊢ ∀ 𝑛 ∈ ℤ ∀ 𝑥 ∈ 𝐵 if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ∈ ( { 0 } ∪ ( ( ran + ∪ 𝐵 ) ∪ ( ran 𝐼 ∪ { ∅ } ) ) )
114	31 32 42 113	mpoexw	⊢ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) ∈ V
115	29 30 114	fvmpt	⊢ ( 𝐺 ∈ V → ( ._g ‘ 𝐺 ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) )
116		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( ._g ‘ 𝐺 ) = ∅ )
117		eqid	⊢ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )
118		fvex	⊢ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ V
119		fvex	⊢ ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ∈ V
120	118 119	ifex	⊢ if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ∈ V
121	44 120	ifex	⊢ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ∈ V
122	117 121	fnmpoi	⊢ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ( ℤ × 𝐵 )
123		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
124	1 123	eqtrid	⊢ ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
125	124	xpeq2d	⊢ ( ¬ 𝐺 ∈ V → ( ℤ × 𝐵 ) = ( ℤ × ∅ ) )
126		xp0	⊢ ( ℤ × ∅ ) = ∅
127	125 126	eqtrdi	⊢ ( ¬ 𝐺 ∈ V → ( ℤ × 𝐵 ) = ∅ )
128	127	fneq2d	⊢ ( ¬ 𝐺 ∈ V → ( ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ( ℤ × 𝐵 ) ↔ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ∅ ) )
129	122 128	mpbii	⊢ ( ¬ 𝐺 ∈ V → ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ∅ )
130		fn0	⊢ ( ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ∅ ↔ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) = ∅ )
131	129 130	sylib	⊢ ( ¬ 𝐺 ∈ V → ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) = ∅ )
132	116 131	eqtr4d	⊢ ( ¬ 𝐺 ∈ V → ( ._g ‘ 𝐺 ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) )
133	115 132	pm2.61i	⊢ ( ._g ‘ 𝐺 ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )
134	5 133	eqtri	⊢ · = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )

Metamath Proof Explorer

Theorem mulgfval

Proof