| 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 |
|
ffvelcdm |
⊢ ( ( 𝑓 : ( 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 ‘ 𝐶 ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 ) |