Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgval.p ⊢ + = ( +g ‘ 𝐺 )
mulgval.o ⊢ 0 = ( 0g ‘ 𝐺 )
mulgval.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
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 = ( 0g ‘ 𝐺 )
4 mulgval.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
5 mulgval.t ⊢ · = ( .g ‘ 𝐺 )
6 eqidd ⊢ ( 𝑤 = 𝐺 → ℤ = ℤ )
7 fveq2 ⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐺 ) )
8 7 1 eqtr4di ⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = 𝐵 )
9 fveq2 ⊢ ( 𝑤 = 𝐺 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝐺 ) )
10 9 3 eqtr4di ⊢ ( 𝑤 = 𝐺 → ( 0g ‘ 𝑤 ) = 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 ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( invg ‘ 𝑤 ) = ( invg ‘ 𝐺 ) )
23 22 4 eqtr4di ⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( invg ‘ 𝑤 ) = 𝐼 )
24 19 fveq1d ⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( 𝑠 ‘ - 𝑛 ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) )
25 23 24 fveq12d ⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) = ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) )
26 20 25 ifeq12d ⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) = if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) )
27 14 26 csbied ⊢ ( 𝑤 = 𝐺 → ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) = if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) )
28 10 27 ifeq12d ⊢ ( 𝑤 = 𝐺 → if ( 𝑛 = 0 , ( 0g ‘ 𝑤 ) , ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) = if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )
29 6 8 28 mpoeq123dv ⊢ ( 𝑤 = 𝐺 → ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑤 ) , ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) )
30 df-mulg ⊢ .g = ( 𝑤 ∈ V ↦ ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑤 ) , ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) )
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 sseldi ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑛 = 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 syl5eq ⊢ ( ¬ 𝐺 ∈ 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 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )