Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ ) |
2 |
|
simpr |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝐴 ) → 𝑛 ∈ 𝐴 ) |
3 |
|
simplll |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) |
4 |
|
nfcv |
⊢ Ⅎ 𝑘 I |
5 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐵 |
6 |
4 5
|
nffv |
⊢ Ⅎ 𝑘 ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) |
7 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐶 |
8 |
4 7
|
nffv |
⊢ Ⅎ 𝑘 ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) |
9 |
6 8
|
nfeq |
⊢ Ⅎ 𝑘 ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) |
10 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑛 → 𝐵 = ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) |
11 |
10
|
fveq2d |
⊢ ( 𝑘 = 𝑛 → ( I ‘ 𝐵 ) = ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) ) |
12 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑛 → 𝐶 = ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) |
13 |
12
|
fveq2d |
⊢ ( 𝑘 = 𝑛 → ( I ‘ 𝐶 ) = ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) ) |
14 |
11 13
|
eqeq12d |
⊢ ( 𝑘 = 𝑛 → ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ↔ ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) ) ) |
15 |
9 14
|
rspc |
⊢ ( 𝑛 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) ) ) |
16 |
2 3 15
|
sylc |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝐴 ) → ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) ) |
17 |
16
|
ifeq1da |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → if ( 𝑛 ∈ 𝐴 , ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) , ( I ‘ 0 ) ) = if ( 𝑛 ∈ 𝐴 , ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) , ( I ‘ 0 ) ) ) |
18 |
|
fvif |
⊢ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) = if ( 𝑛 ∈ 𝐴 , ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐵 ) , ( I ‘ 0 ) ) |
19 |
|
fvif |
⊢ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) = if ( 𝑛 ∈ 𝐴 , ( I ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐶 ) , ( I ‘ 0 ) ) |
20 |
17 18 19
|
3eqtr4g |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) = ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) |
21 |
20
|
mpteq2dv |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ) |
22 |
21
|
fveq1d |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ‘ 𝑥 ) ) |
23 |
|
eqid |
⊢ ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) |
24 |
|
eqid |
⊢ ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) |
25 |
23 24
|
fvmptex |
⊢ ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ‘ 𝑥 ) |
26 |
|
eqid |
⊢ ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) |
27 |
|
eqid |
⊢ ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) |
28 |
26 27
|
fvmptex |
⊢ ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ‘ 𝑥 ) |
29 |
22 25 28
|
3eqtr4g |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ‘ 𝑥 ) ) |
30 |
1 29
|
seqfeq |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) = seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ) |
31 |
30
|
breq1d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) |
32 |
31
|
anbi2d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) ) |
33 |
32
|
rexbidva |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) ) |
34 |
|
simplr |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝑚 ∈ ℕ ) |
35 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
36 |
34 35
|
eleqtrdi |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) ) |
37 |
|
f1of |
⊢ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 ) |
38 |
37
|
ad2antlr |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 ) |
39 |
|
ffvelrn |
⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) |
40 |
38 39
|
sylancom |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) |
41 |
|
simplll |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) |
42 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) |
43 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) |
44 |
42 43
|
nfeq |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) |
45 |
|
csbeq1a |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) ) |
46 |
|
csbeq1a |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( I ‘ 𝐶 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) |
47 |
45 46
|
eqeq12d |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ↔ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) ) |
48 |
44 47
|
rspc |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) ) |
49 |
40 41 48
|
sylc |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) |
50 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑥 ) ∈ V |
51 |
|
csbfv2g |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) ) |
52 |
50 51
|
ax-mp |
⊢ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) |
53 |
|
csbfv2g |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
54 |
50 53
|
ax-mp |
⊢ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) |
55 |
49 52 54
|
3eqtr3g |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
56 |
|
elfznn |
⊢ ( 𝑥 ∈ ( 1 ... 𝑚 ) → 𝑥 ∈ ℕ ) |
57 |
56
|
adantl |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑥 ∈ ℕ ) |
58 |
|
fveq2 |
⊢ ( 𝑛 = 𝑥 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑥 ) ) |
59 |
58
|
csbeq1d |
⊢ ( 𝑛 = 𝑥 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) |
60 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
61 |
59 60
|
fvmpti |
⊢ ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) ) |
62 |
57 61
|
syl |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) ) |
63 |
58
|
csbeq1d |
⊢ ( 𝑛 = 𝑥 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) |
64 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) |
65 |
63 64
|
fvmpti |
⊢ ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
66 |
57 65
|
syl |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
67 |
55 62 66
|
3eqtr4d |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) ) |
68 |
36 67
|
seqfveq |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) |
69 |
68
|
eqeq2d |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) |
70 |
69
|
pm5.32da |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
71 |
70
|
exbidv |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
72 |
71
|
rexbidva |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
73 |
33 72
|
orbi12d |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) ) |
74 |
73
|
iotabidv |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) ) |
75 |
|
df-sum |
⊢ Σ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) |
76 |
|
df-sum |
⊢ Σ 𝑘 ∈ 𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
77 |
74 75 76
|
3eqtr4g |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 ) |