Step |
Hyp |
Ref |
Expression |
1 |
|
hbtlem.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
hbtlem.u |
⊢ 𝑈 = ( LIdeal ‘ 𝑃 ) |
3 |
|
hbtlem.s |
⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 ) |
4 |
|
hbtlem6.n |
⊢ 𝑁 = ( RSpan ‘ 𝑃 ) |
5 |
|
hbtlem6.r |
⊢ ( 𝜑 → 𝑅 ∈ LNoeR ) |
6 |
|
hbtlem6.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑈 ) |
7 |
|
hbtlem6.x |
⊢ ( 𝜑 → 𝑋 ∈ ℕ0 ) |
8 |
|
lnrring |
⊢ ( 𝑅 ∈ LNoeR → 𝑅 ∈ Ring ) |
9 |
5 8
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
10 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
11 |
1 2 3 10
|
hbtlem2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
12 |
9 6 7 11
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
13 |
|
eqid |
⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 ) |
14 |
10 13
|
lnr2i |
⊢ ( ( 𝑅 ∈ LNoeR ∧ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ) → ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ) |
15 |
5 12 14
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ) |
16 |
|
elfpw |
⊢ ( 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ↔ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) |
17 |
|
fvex |
⊢ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ∈ V |
18 |
|
eqid |
⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) |
19 |
17 18
|
fnmpti |
⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } |
20 |
19
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) |
21 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ) |
22 |
|
eqid |
⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 ) |
23 |
1 2 3 22
|
hbtlem1 |
⊢ ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) |
24 |
5 6 7 23
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) |
25 |
18
|
rnmpt |
⊢ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑑 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) } |
26 |
|
fveq2 |
⊢ ( 𝑐 = 𝑏 → ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) = ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ) |
27 |
26
|
breq1d |
⊢ ( 𝑐 = 𝑏 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ) ) |
28 |
27
|
rexrab |
⊢ ( ∃ 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
29 |
28
|
abbii |
⊢ { 𝑑 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) } = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } |
30 |
25 29
|
eqtri |
⊢ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } |
31 |
24 30
|
eqtr4di |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
32 |
31
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
33 |
21 32
|
sseqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
34 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ∈ Fin ) |
35 |
|
fipreima |
⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑎 ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ∧ 𝑎 ∈ Fin ) → ∃ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) |
36 |
20 33 34 35
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) |
37 |
|
elfpw |
⊢ ( 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ↔ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) |
38 |
|
ssrab2 |
⊢ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ⊆ 𝐼 |
39 |
|
sstr2 |
⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ( { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ⊆ 𝐼 → 𝑘 ⊆ 𝐼 ) ) |
40 |
38 39
|
mpi |
⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → 𝑘 ⊆ 𝐼 ) |
41 |
40
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) → 𝑘 ⊆ 𝐼 ) |
42 |
|
velpw |
⊢ ( 𝑘 ∈ 𝒫 𝐼 ↔ 𝑘 ⊆ 𝐼 ) |
43 |
41 42
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) → 𝑘 ∈ 𝒫 𝐼 ) |
44 |
43
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ 𝒫 𝐼 ) |
45 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ Fin ) |
46 |
44 45
|
elind |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ) |
47 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑅 ∈ Ring ) |
48 |
1
|
ply1ring |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring ) |
49 |
9 48
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ Ring ) |
50 |
49
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑃 ∈ Ring ) |
51 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) |
52 |
51 38
|
sstrdi |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ 𝐼 ) |
53 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
54 |
53 2
|
lidlss |
⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) ) |
55 |
6 54
|
syl |
⊢ ( 𝜑 → 𝐼 ⊆ ( Base ‘ 𝑃 ) ) |
56 |
55
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) ) |
57 |
52 56
|
sstrd |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ ( Base ‘ 𝑃 ) ) |
58 |
4 53 2
|
rspcl |
⊢ ( ( 𝑃 ∈ Ring ∧ 𝑘 ⊆ ( Base ‘ 𝑃 ) ) → ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 ) |
59 |
50 57 58
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 ) |
60 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑋 ∈ ℕ0 ) |
61 |
1 2 3 10
|
hbtlem2 |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
62 |
47 59 60 61
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
63 |
|
df-ima |
⊢ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = ran ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) |
64 |
4 53
|
rspssid |
⊢ ( ( 𝑃 ∈ Ring ∧ 𝑘 ⊆ ( Base ‘ 𝑃 ) ) → 𝑘 ⊆ ( 𝑁 ‘ 𝑘 ) ) |
65 |
50 57 64
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ ( 𝑁 ‘ 𝑘 ) ) |
66 |
|
ssrab |
⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↔ ( 𝑘 ⊆ 𝐼 ∧ ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) ) |
67 |
66
|
simprbi |
⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) |
68 |
67
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) |
69 |
|
ssrab |
⊢ ( 𝑘 ⊆ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↔ ( 𝑘 ⊆ ( 𝑁 ‘ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) ) |
70 |
65 68 69
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) |
71 |
70
|
resmptd |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏 ∈ 𝑘 ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
72 |
|
resmpt |
⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏 ∈ 𝑘 ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
73 |
72
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏 ∈ 𝑘 ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
74 |
71 73
|
eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ) |
75 |
|
resss |
⊢ ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) |
76 |
74 75
|
eqsstrrdi |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
77 |
|
rnss |
⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) → ran ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
78 |
76 77
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ran ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
79 |
63 78
|
eqsstrid |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
80 |
1 2 3 22
|
hbtlem1 |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) |
81 |
47 59 60 80
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) |
82 |
|
eqid |
⊢ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) |
83 |
82
|
rnmpt |
⊢ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑒 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) } |
84 |
27
|
rexrab |
⊢ ( ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
85 |
84
|
abbii |
⊢ { 𝑒 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) } = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } |
86 |
83 85
|
eqtri |
⊢ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } |
87 |
81 86
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) |
88 |
79 87
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) |
89 |
13 10
|
rspssp |
⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) |
90 |
47 62 88 89
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) |
91 |
46 90
|
jca |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) |
92 |
|
fveq2 |
⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ) |
93 |
92
|
sseq1d |
⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) |
94 |
93
|
anbi2d |
⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ↔ ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) ) |
95 |
91 94
|
syl5ibcom |
⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) ) |
96 |
37 95
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ) → ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) ) |
97 |
96
|
expimpd |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ∧ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) ) |
98 |
97
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ( 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ∧ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) ) |
99 |
98
|
reximdv2 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ∃ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) |
100 |
36 99
|
mpd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) |
101 |
16 100
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) |
102 |
|
sseq1 |
⊢ ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) |
103 |
102
|
rexbidv |
⊢ ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ( ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ↔ ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) |
104 |
101 103
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ) → ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) |
105 |
104
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) |
106 |
15 105
|
mpd |
⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) |